# 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 ***)