| changeset 12415 | 74977582a585 |
| parent 11270 | a315a3862bb4 |
| child 13507 | febb8e5d2a9d |
| 12414:61e1681b0b5d | 12415:74977582a585 |
|---|---|
55 Method.ctxt_args (fn ctxt => |
55 Method.ctxt_args (fn ctxt => |
56 Method.METHOD (fn facts => |
56 Method.METHOD (fn facts => |
57 gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} |
57 gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} |
58 "for proving possibility theorems" |
58 "for proving possibility theorems" |
59 |
59 |
60 lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)" |
|
61 by (induct e, auto simp: knows_Cons) |
|
62 |
|
60 end |
63 end |