Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Atoms.thy
changeset 2597 0f289a52edbe
parent 2568 8193bbaa07fe
child 2744 56b8d977d1c0
equal deleted inserted replaced
2596:9fa37acdb2ce 2597:0f289a52edbe 
   195   by simp
 
   195   by simp
 
   196 
   196 
   197 
   197 
   198 section {* Tests with subtyping and automatic coercions *}
 
   198 section {* Tests with subtyping and automatic coercions *}
 
   199 
   199 
   200 setup Subtyping.setup
 
   200 declare [[coercion_enabled]]
 
   201 
   201 
   202 atom_decl var1
 
   202 atom_decl var1
 
   203 atom_decl var2
 
   203 atom_decl var2
 
   204 
   204 
   205 declare [[coercion "atom::var1\<Rightarrow>atom"]]
 
   205 declare [[coercion "atom::var1\<Rightarrow>atom"]]
nominal2