--- a/src/Pure/Isar/method.ML Thu Mar 02 18:18:10 2000 +0100
+++ b/src/Pure/Isar/method.ML Thu Mar 02 18:18:31 2000 +0100
@@ -301,9 +301,9 @@
fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt);
-(* res_inst tactic emulation *)
+(* res_inst_tac emulations *)
-(*Note: insts refer to the hidden (!) goal context; use with care*)
+(*Note: insts refer to the implicit (!) goal context; use at your own risk*)
fun gen_res_inst tac ((i, insts), thm) =
METHOD (fn facts => (insert_tac facts THEN' tac insts thm) i);
@@ -313,6 +313,14 @@
val forw_inst = gen_res_inst Tactic.forw_inst_tac;
+(* simple Prolog interpreter *)
+
+fun prolog_tac rules facts =
+ DEPTH_SOLVE_1 (HEADGOAL (Tactic.assume_tac APPEND' Tactic.resolve_tac (facts @ rules)));
+
+val prolog = METHOD o prolog_tac;
+
+
(** methods theory data **)
@@ -547,7 +555,8 @@
("res_inst_tac", inst_args res_inst, "res_inst_tac emulation (beware!)"),
("eres_inst_tac", inst_args eres_inst, "eres_inst_tac emulation (beware!)"),
("dres_inst_tac", inst_args dres_inst, "dres_inst_tac emulation (beware!)"),
- ("forw_inst_tac", inst_args forw_inst, "forw_inst_tac emulation (beware!)")];
+ ("forw_inst_tac", inst_args forw_inst, "forw_inst_tac emulation (beware!)"),
+ ("prolog", thms_args prolog, "simple prolog interpreter")];
(* setup *)