equal
deleted
inserted
replaced
169 | discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm)) |
169 | discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm)) |
170 |
170 |
171 fun by_tac ctxt thms ns ts t tac = |
171 fun by_tac ctxt thms ns ts t tac = |
172 Goal.prove ctxt [] (map as_prop ts) (as_prop t) |
172 Goal.prove ctxt [] (map as_prop ts) (as_prop t) |
173 (fn {context, prems} => HEADGOAL (tac context prems)) |
173 (fn {context, prems} => HEADGOAL (tac context prems)) |
174 |> Drule.generalize ([], ns) |
174 |> Drule.generalize (Symtab.empty, Symtab.make_set ns) |
175 |> discharge 1 thms |
175 |> discharge 1 thms |
176 |
176 |
177 fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac) |
177 fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac) |
178 |
178 |
179 |
179 |