--- a/src/HOL/Auth/Event.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Event.ML Fri Oct 17 15:25:12 1997 +0200
@@ -46,7 +46,7 @@
qed "spies_subset_spies_Says";
goal thy "spies evs <= spies (Notes A X # evs)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Fast_tac 1);
qed "spies_subset_spies_Notes";
@@ -54,14 +54,14 @@
goal thy "Says A B X : set evs --> X : spies evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
- (!simpset setloop split_tac [expand_event_case, expand_if])));
+ (!simpset addsplits [expand_event_case, expand_if])));
qed_spec_mp "Says_imp_spies";
(*Spy sees Notes of bad agents*)
goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
- (!simpset setloop split_tac [expand_event_case, expand_if])));
+ (!simpset addsplits [expand_event_case, expand_if])));
qed_spec_mp "Notes_imp_spies";
(*Use with addSEs to derive contradictions from old Says events containing
@@ -80,7 +80,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [parts_insert_spies]
- setloop split_tac [expand_event_case, expand_if])));
+ addsplits [expand_event_case, expand_if])));
by (ALLGOALS Blast_tac);
qed "parts_spies_subset_used";
@@ -91,7 +91,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [parts_insert_spies]
- setloop split_tac [expand_event_case, expand_if])));
+ addsplits [expand_event_case, expand_if])));
by (ALLGOALS Blast_tac);
bind_thm ("initState_into_used", impOfSubs (result()));