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/Nat.thy
changeset 20380 14f9f2a1caa6
parent 20355 50aaae6ae4db
child 20588 c847c56edf0c
equal deleted inserted replaced
20379:154d8c155a65 20380:14f9f2a1caa6 
  1045 
  1045 
  1046 lemma one_is_suc_zero [code inline]:
 
  1046 lemma one_is_suc_zero [code inline]:
 
  1047   "1 = Suc 0"
 
  1047   "1 = Suc 0"
 
  1048   by simp
 
  1048   by simp
 
  1049 
  1049 
  1050 code_alias
 
       
  1051   "nat" "Nat.nat"
 
       
  1052   "0" "Nat.Zero"
 
       
  1053   "1" "Nat.One"
 
       
  1054   "Suc" "Nat.Suc"
 
       
  1055 
       
  1056 end
 
  1050 end
isabelle