| changeset 10832 | e33b47e4246d |
| parent 10212 | 33fe2d701ddd |
| child 11326 | 680ebd093cfe |
--- a/src/HOL/NatDef.thy Tue Jan 09 15:18:07 2001 +0100 +++ b/src/HOL/NatDef.thy Tue Jan 09 15:22:13 2001 +0100 @@ -36,7 +36,7 @@ (* type definition *) typedef (Nat) - nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" (lfp_def) + nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep`X))" (lfp_def) instance nat :: {ord, zero}