--- a/src/HOL/Auth/Message.ML Mon Apr 14 10:28:21 1997 +0200
+++ b/src/HOL/Auth/Message.ML Tue Apr 15 10:15:09 1997 +0200
@@ -7,17 +7,6 @@
Inductive relations "parts", "analz" and "synth"
*)
-val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
-by (case_tac "P" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
-val expand_case = result();
-
-fun expand_case_tac P i =
- res_inst_tac [("P",P)] expand_case i THEN
- Simp_tac (i+1) THEN
- Simp_tac i;
-
-
open Message;
AddIffs (msg.inject);
--- a/src/HOL/simpdata.ML Mon Apr 14 10:28:21 1997 +0200
+++ b/src/HOL/simpdata.ML Tue Apr 15 10:15:09 1997 +0200
@@ -317,6 +317,17 @@
(fn _ => [rtac ext 1, rtac refl 1]);
+val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
+by (case_tac "P" 1);
+by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
+val expand_case = result();
+
+fun expand_case_tac P i =
+ res_inst_tac [("P",P)] expand_case i THEN
+ Simp_tac (i+1) THEN
+ Simp_tac i;
+
+
(*** Install simpsets and datatypes in theory structure ***)