Skip to content

Commit

Permalink
Fix case of theory declared in hilbertScript.sml
Browse files Browse the repository at this point in the history
  • Loading branch information
@mn200
mn200 committed Jan 29, 2025
1 parent e6ea888 commit c4bc6cd
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion examples/axiomatic-developments/geometry/hilbertScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ open HolKernel Parse boolLib bossLib;
open pred_setTheory;
open listTheory;

val _ = new_theory "Hilbert";
val _ = new_theory "hilbert";

(* Useful definition/s *)
Definition only_one_def:
Expand Down

0 comments on commit c4bc6cd

Please sign in to comment.