[isabelle] Trying to rename Lattices.thy
I'm trying to rename HOL/Lattices.thy so I can load it, experiment with
it, and mark it up, but it's picky about what it's name can be.
I renamed the first three HOL theories, replaced any use commands in
them, such as `use "Tools/abel_cancel.ML"`, with the actual ML, and
replaced any fully qualified names with the new theory name.
They all load without any errors. The renaming is like this:
HOL.thy is renamed i12H02hol_0ed.thy
Orderings.thy is renamed i12H03ord_0ed.thy
Groups.thy is renamed i12H04grp_0ed.thy
I try to rename Lattices.thy, but it appears that the main requirement
is that the first letter of the name be capital "L". Names that have
worked are these:
If the first letter of the name is lowercase, such as "lattices.thy" or
"iLattices.thy", it gets down to line 75,
"class.semilattice_inf sup greater_eq greater"
and it gives this error:
Type unification failed: No type arity HOL.bool :: iLattices.sup
Failed to meet type constraint:
Term: op ⊔ :: (??'a∷iLattices.sup ⇒ (??'a∷iLattices.sup ⇒
Type: (HOL.bool ⇒ (HOL.bool ⇒ HOL.bool))
If the first letter of the name is capitalized, but not "L", such as
"Attices.thy", it gets to line 431,
and gives the error:
Type unification failed: Occurs check! [and so forth]
It's no big deal. It just messes up my naming scheme, and the fact that
I've renamed the other three files causes me to wonder about this.
If there's no problem, maybe someone can at least tell me something
like, "Yea, don't do that".
This archive was generated by a fusion of
Pipermail (Mailman edition) and