changeset 8943 | a4f8be72f585 |
parent 7872 | 2e2d7e80fb07 |
child 10212 | 33fe2d701ddd |
--- a/src/HOL/NatDef.thy Tue May 23 18:28:11 2000 +0200 +++ b/src/HOL/NatDef.thy Tue May 23 18:29:17 2000 +0200 @@ -39,13 +39,12 @@ nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" (lfp_def) instance - nat :: ord + nat :: {ord, zero} (* abstract constants and syntax *) consts - "0" :: nat ("0") Suc :: nat => nat pred_nat :: "(nat * nat) set"