author | paulson |
Wed, 24 Sep 1997 12:24:41 +0200 (1997-09-24) | |
changeset 3701 | 6f0ed3eef1a9 |
parent 3700 | 3a8192e83579 |
child 3702 | 0fc9bf467f95 |
--- a/src/HOL/Auth/Event.ML Wed Sep 24 10:51:52 1997 +0200 +++ b/src/HOL/Auth/Event.ML Wed Sep 24 12:24:41 1997 +0200 @@ -82,7 +82,9 @@ (!simpset addsimps [parts_insert_spies] setloop split_tac [expand_event_case, expand_if]))); by (ALLGOALS Blast_tac); -bind_thm ("usedI", impOfSubs (result())); +qed "parts_spies_subset_used"; + +bind_thm ("usedI", impOfSubs parts_spies_subset_used); AddIs [usedI]; goal thy "parts (initState B) <= used evs";