1.1 --- a/src/Pure/Isar/method.ML	Thu Mar 02 18:18:10 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Mar 02 18:18:31 2000 +0100
     1.3 @@ -301,9 +301,9 @@
     1.4  fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt);
     1.5  
     1.6  
     1.7 -(* res_inst tactic emulation *)
     1.8 +(* res_inst_tac emulations *)
     1.9  
    1.10 -(*Note: insts refer to the hidden (!) goal context; use with care*)
    1.11 +(*Note: insts refer to the implicit (!) goal context; use at your own risk*)
    1.12  fun gen_res_inst tac ((i, insts), thm) =
    1.13    METHOD (fn facts => (insert_tac facts THEN' tac insts thm) i);
    1.14  
    1.15 @@ -313,6 +313,14 @@
    1.16  val forw_inst = gen_res_inst Tactic.forw_inst_tac;
    1.17  
    1.18  
    1.19 +(* simple Prolog interpreter *)
    1.20 +
    1.21 +fun prolog_tac rules facts =
    1.22 +  DEPTH_SOLVE_1 (HEADGOAL (Tactic.assume_tac APPEND' Tactic.resolve_tac (facts @ rules)));
    1.23 +
    1.24 +val prolog = METHOD o prolog_tac;
    1.25 +
    1.26 +
    1.27  
    1.28  (** methods theory data **)
    1.29  
    1.30 @@ -547,7 +555,8 @@
    1.31    ("res_inst_tac", inst_args res_inst, "res_inst_tac emulation (beware!)"),
    1.32    ("eres_inst_tac", inst_args eres_inst, "eres_inst_tac emulation (beware!)"),
    1.33    ("dres_inst_tac", inst_args dres_inst, "dres_inst_tac emulation (beware!)"),
    1.34 -  ("forw_inst_tac", inst_args forw_inst, "forw_inst_tac emulation (beware!)")];
    1.35 +  ("forw_inst_tac", inst_args forw_inst, "forw_inst_tac emulation (beware!)"),
    1.36 +  ("prolog", thms_args prolog, "simple prolog interpreter")];
    1.37  
    1.38  
    1.39  (* setup *)