# HG changeset patch # User berghofe # Date 1149779089 -7200 # Node ID f1dccc547595b832387dea0d337dd609d0b5ca38 # Parent e9e9be6111bb893c7c3fc5aa0dfef93da107e4d0 Removed "code del" declarations again. diff -r e9e9be6111bb -r f1dccc547595 src/HOL/Library/EfficientNat.thy --- a/src/HOL/Library/EfficientNat.thy Thu Jun 08 15:25:07 2006 +0200 +++ b/src/HOL/Library/EfficientNat.thy Thu Jun 08 17:04:49 2006 +0200 @@ -85,13 +85,6 @@ using their counterparts on the integers: *} -declare - Nat.plus.simps [code del] - Nat.minus.simps [code del] - diff_0_eq_0 [code del] - diff_Suc_Suc [code del] - Nat.times.simps [code del] - lemma [code]: "m + n = nat (int m + int n)" by arith lemma [code]: "m - n = nat (int m - int n)" @@ -218,7 +211,7 @@ (Drule.instantiate' [] [SOME (cert (lambda v (Abs ("x", HOLogic.natT, abstract_over (Sucv, - (HOLogic.dest_Trueprop o prop_of) th'))))), + HOLogic.dest_Trueprop (prop_of th')))))), SOME (cert v)] Suc_clause')) (Thm.forall_intr (cert v) th')) in @@ -229,7 +222,7 @@ fun clause_suc_preproc thy ths = let - val dest = fst o HOLogic.dest_mem o ObjectLogic.drop_judgment thy + val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop in if forall (can (dest o concl_of)) ths andalso exists (fn th => member (op =) (foldr add_term_consts