equal
deleted
inserted
replaced
35 inj_pubK: "inj pubK" |
35 inj_pubK: "inj pubK" |
36 priK_neq_pubK: "priK A ~= pubK B" |
36 priK_neq_pubK: "priK A ~= pubK B" |
37 |
37 |
38 use "Public_lemmas.ML" |
38 use "Public_lemmas.ML" |
39 |
39 |
|
40 lemma [simp]: "K \\<in> symKeys ==> invKey K = K" |
|
41 by (simp add: symKeys_def) |
|
42 |
40 (*Specialized methods*) |
43 (*Specialized methods*) |
41 |
44 |
42 method_setup possibility = {* |
45 method_setup possibility = {* |
43 Method.ctxt_args (fn ctxt => |
46 Method.ctxt_args (fn ctxt => |
44 Method.METHOD (fn facts => |
47 Method.METHOD (fn facts => |