Re: [isabelle] Type parameters in a locale? Datatypes in a locale?

Hi all,

> theory testing imports Main begin   (** nothing up my sleeve **)
> thm le_supI1                        (* some theorem from semilattice_sup *)
> Prints out
> (?x\<Colon>?'a\<Colon>semilattice_sup) \<le>
> (?a\<Colon>?'a\<Colon>semilattice_sup) \<Longrightarrow>
> ?x \<le> sup ?a (?b\<Colon>?'a\<Colon>semilattice_sup)
> Why?  The notation
> \<le>  (from class order) is preserved, but the notation "\<squnion>"
> for sup (from
> class semilattice_sup is gone.

I guess the source for the misunderstanding is that the lattice syntax
for sup etc. is deleted in theory Lattices; to obtain it again, import
theory Lattice_Syntax.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.