# HG changeset patch
# User paulson
# Date 861092109 -7200
# Node ID f18035b1d531fa3ae5d80c2d9517a9adcf5f9f35
# Parent  abca00c27841e13b59bd994dc4215e139a6e0d1e
Moved expand_case_tac from Auth/Message.ML to simpdata.ML

diff -r abca00c27841 -r f18035b1d531 src/HOL/Auth/Message.ML
--- 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);
diff -r abca00c27841 -r f18035b1d531 src/HOL/simpdata.ML
--- 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 ***)