src/Pure/Isar/method.ML
changeset 7574 5bcb7fc31caa
parent 7555 dd281afb33d7
child 7601 c568799bf21b
     1.1 --- a/src/Pure/Isar/method.ML	Wed Sep 22 20:58:23 1999 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Sep 22 20:59:22 1999 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    val fail: Proof.method
     1.5    val succeed: Proof.method
     1.6    val insert_tac: thm list -> int -> tactic
     1.7 +  val insert: thm list -> Proof.method
     1.8    val insert_facts: Proof.method
     1.9    val fold: thm list -> Proof.method
    1.10    val unfold: thm list -> Proof.method
    1.11 @@ -110,6 +111,7 @@
    1.12    | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
    1.13  
    1.14  val insert_facts = METHOD (ALLGOALS o insert_tac);
    1.15 +fun insert thms = METHOD (fn facts => ALLGOALS (insert_tac (thms @ facts)));
    1.16  
    1.17  end;
    1.18  
    1.19 @@ -378,7 +380,8 @@
    1.20  val pure_methods =
    1.21   [("fail", no_args fail, "force failure"),
    1.22    ("succeed", no_args succeed, "succeed"),
    1.23 -  ("-", no_args insert_facts, "insert facts"),
    1.24 +  ("-", no_args insert_facts, "do nothing, inserting current facts only"),
    1.25 +  ("insert", thms_args insert, "insert facts (improper!)"),
    1.26    ("fold", thms_args fold, "fold definitions, ignoring facts"),
    1.27    ("unfold", thms_args unfold, "unfold definitions, ignoring facts"),
    1.28    ("rule", thms_args rule, "apply some rule"),