Mercurial Mercurial > repos > isabelle / 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.
src/HOL/Main.thy
changeset 13093 ab0335307905
parent 12554 671b4d632c34
child 13367 ad307f0d80db
equal deleted inserted replaced
13092:eae72c47d07f 13093:ab0335307905 
   114   "snd"     ("snd")
 
   114   "snd"     ("snd")
 
   115 
   115 
   116   "Nil"     ("[]")
 
   116   "Nil"     ("[]")
 
   117   "Cons"    ("(_ ::/ _)")
 
   117   "Cons"    ("(_ ::/ _)")
 
   118 
   118 
       
   119   "wfrec"   ("wf'_rec?")
 
       
   120 
       
   121 ML {* fun wf_rec f x = f (wf_rec f) x; *}
 
       
   122 
   119 lemma [code]: "((n::nat) < 0) = False" by simp
 
   123 lemma [code]: "((n::nat) < 0) = False" by simp
 
   120 declare less_Suc_eq [code]
 
   124 declare less_Suc_eq [code]
 
   121 
   125 
   122 end
 
   126 end
isabelle