equal
deleted
inserted
replaced
48 consts N :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *) |
48 consts N :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *) |
49 consts pred :: fname |
49 consts pred :: fname |
50 consts suc :: mname |
50 consts suc :: mname |
51 add :: mname |
51 add :: mname |
52 consts any :: vname |
52 consts any :: vname |
53 syntax dummy:: expr ("<>") |
53 |
54 one :: expr |
54 abbreviation |
55 translations |
55 dummy :: expr ("<>") |
56 "<>" == "LAcc any" |
56 where "<> == LAcc any" |
57 "one" == "{Nat}new Nat..suc(<>)" |
57 |
|
58 abbreviation |
|
59 one :: expr |
|
60 where "one == {Nat}new Nat..suc(<>)" |
58 |
61 |
59 text {* The following properties could be derived from a more complete |
62 text {* The following properties could be derived from a more complete |
60 program model, which we leave out for laziness. *} |
63 program model, which we leave out for laziness. *} |
61 |
64 |
62 axioms Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)" |
65 axioms Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)" |