equal
deleted
inserted
replaced
554 |
554 |
555 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. |
555 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. |
556 Function mkcl converts theorems to clauses.*) |
556 Function mkcl converts theorems to clauses.*) |
557 fun MESON mkcl cltac i st = |
557 fun MESON mkcl cltac i st = |
558 SELECT_GOAL |
558 SELECT_GOAL |
559 (EVERY [ObjectLogic.atomize_tac 1, |
559 (EVERY [ObjectLogic.atomize_prems_tac 1, |
560 rtac ccontr 1, |
560 rtac ccontr 1, |
561 METAHYPS (fn negs => |
561 METAHYPS (fn negs => |
562 EVERY1 [skolemize_prems_tac negs, |
562 EVERY1 [skolemize_prems_tac negs, |
563 METAHYPS (cltac o mkcl)]) 1]) i st |
563 METAHYPS (cltac o mkcl)]) 1]) i st |
564 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) |
564 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) |