| changeset 6775 | 9d96ce9c27d6 |
| parent 6736 | a0b2cfa12d0d |
| child 6849 | 0b660860c0ad |
--- a/src/Pure/Isar/method.ML Fri Jun 04 19:54:38 1999 +0200 +++ b/src/Pure/Isar/method.ML Fri Jun 04 19:54:54 1999 +0200 @@ -14,6 +14,7 @@ signature METHOD = sig include BASIC_METHOD + val multi_resolve: thm list -> thm -> thm Seq.seq val FINISHED: tactic -> tactic val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * thm list) list) Seq.seq val METHOD: (thm list -> tactic) -> Proof.method