src/HOL/Auth/OtwayRees_AN.ML
changeset 2637 e9b203f854ae
parent 2516 4d68fbe6378b
child 2837 dee1c7f1f576
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Sat Feb 15 17:48:19 1997 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Sat Feb 15 17:52:31 1997 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4        (!claset addIs [impOfSubs analz_subset_parts]
     1.5                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
     1.6                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     1.7 -               addss (!simpset)) 1);
     1.8 +               unsafe_addss (!simpset)) 1);
     1.9  (*OR3*)
    1.10  by (fast_tac (!claset addss (!simpset)) 1);
    1.11  qed_spec_mp "new_keys_not_used";
    1.12 @@ -297,7 +297,7 @@
    1.13                        addIs [impOfSubs analz_subset_parts]
    1.14                        addss (!simpset addsimps [parts_insert2])) 2);
    1.15  (*Oops*) 
    1.16 -by (best_tac (!claset addDs [unique_session_keys] addss (!simpset)) 3);
    1.17 +by (best_tac (!claset addDs [unique_session_keys] unsafe_addss (!simpset)) 3);
    1.18  (*OR4, Fake*) 
    1.19  by (REPEAT_FIRST spy_analz_tac);
    1.20  val lemma = result() RS mp RS mp RSN(2,rev_notE);