equal
deleted
inserted
replaced
37 use "Shared_lemmas.ML" |
37 use "Shared_lemmas.ML" |
38 |
38 |
39 (*Lets blast_tac perform this step without needing the simplifier*) |
39 (*Lets blast_tac perform this step without needing the simplifier*) |
40 lemma invKey_shrK_iff [iff]: |
40 lemma invKey_shrK_iff [iff]: |
41 "(Key (invKey K) \<in> X) = (Key K \<in> X)" |
41 "(Key (invKey K) \<in> X) = (Key K \<in> X)" |
42 by auto; |
42 by auto |
43 |
43 |
44 (*Specialized methods*) |
44 (*Specialized methods*) |
45 |
45 |
46 method_setup analz_freshK = {* |
46 method_setup analz_freshK = {* |
47 Method.no_args |
47 Method.no_args |