Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Library/Efficient_Nat.thy
changeset 29730 86cac1fab613
parent 29657 881f328dfbb3
child 29752 9e94b7078fa5
equal deleted inserted replaced
29727:02557b98bd0a 29730:86cac1fab613 
   306 *}
 
   306 *}
 
   307 
   307 
   308 code_reserved Haskell Nat
 
   308 code_reserved Haskell Nat
 
   309 
   309 
   310 code_type nat
 
   310 code_type nat
 
   311   (Haskell "Nat")
 
   311   (Haskell "Nat.Nat")
 
   312 
   312 
   313 code_instance nat :: eq
 
   313 code_instance nat :: eq
 
   314   (Haskell -)
 
   314   (Haskell -)
 
   315 
   315 
   316 text {*
 
   316 text {*
wneuper/isa