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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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