Miniscoping rules are deleted, as these brittle proofs
would otherwise have to be entirely redone
--- a/src/HOL/Lex/AutoChopper.ML Thu Sep 05 10:27:36 1996 +0200
+++ b/src/HOL/Lex/AutoChopper.ML Thu Sep 05 10:29:20 1996 +0200
@@ -6,6 +6,8 @@
Main result: auto_chopper satisfies the is_auto_chopper specification.
*)
+Delsimps (ex_simps @ all_simps);
+
open AutoChopper;
infix repeat_RS;
--- a/src/HOL/MiniML/W.ML Thu Sep 05 10:27:36 1996 +0200
+++ b/src/HOL/MiniML/W.ML Thu Sep 05 10:29:20 1996 +0200
@@ -9,6 +9,7 @@
open W;
Addsimps [Suc_le_lessD];
+Delsimps (ex_simps @ all_simps);
(* correctness of W with respect to has_type *)
goal W.thy