src/HOL/Auth/OtwayRees.ML
changeset 2637 e9b203f854ae
parent 2516 4d68fbe6378b
child 2837 dee1c7f1f576
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Sat Feb 15 17:48:19 1997 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Sat Feb 15 17:52:31 1997 +0100
     1.3 @@ -92,9 +92,9 @@
     1.4               (*Fake message*)
     1.5               TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     1.6                                             impOfSubs Fake_parts_insert]
     1.7 -                                    addss (!simpset)) 2)) THEN
     1.8 +                            unsafe_addss (!simpset)) 2)) THEN
     1.9       (*Base case*)
    1.10 -     fast_tac (!claset addss (!simpset)) 1 THEN
    1.11 +     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
    1.12       ALLGOALS Asm_simp_tac) i;
    1.13  
    1.14  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.15 @@ -134,7 +134,7 @@
    1.16        (!claset addIs [impOfSubs analz_subset_parts]
    1.17                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.18                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.19 -               addss (!simpset)) 1);
    1.20 +               unsafe_addss (!simpset)) 1);
    1.21  (*OR1-3*)
    1.22  by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
    1.23  qed_spec_mp "new_keys_not_used";