--- a/src/HOL/Auth/Shared.thy Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/Shared.thy Fri Mar 13 19:58:26 2009 +0100
@@ -239,20 +239,18 @@
method_setup analz_freshK = {*
Method.ctxt_args (fn ctxt =>
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (Simplifier.context ctxt Shared.analz_image_freshK_ss))]))) *}
"for proving the Session Key Compromise theorem"
method_setup possibility = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
"for proving possibility theorems"
method_setup basic_possibility = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
+ Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
"for proving possibility theorems"
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"