author | paulson |
Tue, 23 May 2000 18:29:17 +0200 | |
changeset 8943 | a4f8be72f585 |
parent 8942 | 6aad5381ba83 |
child 8944 | 96964d43a472 |
--- 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"