equal
deleted
inserted
replaced
232 lemma "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)" |
232 lemma "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)" |
233 by fast |
233 by fast |
234 |
234 |
235 (* disjunction in atom: *) |
235 (* disjunction in atom: *) |
236 lemma "(!P. g P :- (P => b | a)) => g(a | b)" |
236 lemma "(!P. g P :- (P => b | a)) => g(a | b)" |
237 apply (tactic "step_tac HOL_cs 1") |
237 apply (tactic "step_tac (put_claset HOL_cs @{context}) 1") |
238 apply (tactic "step_tac HOL_cs 1") |
238 apply (tactic "step_tac (put_claset HOL_cs @{context}) 1") |
239 apply (tactic "step_tac HOL_cs 1") |
239 apply (tactic "step_tac (put_claset HOL_cs @{context}) 1") |
240 prefer 2 |
240 prefer 2 |
241 apply fast |
241 apply fast |
242 apply fast |
242 apply fast |
243 done |
243 done |
244 |
244 |