src/Pure/drule.ML
changeset 3555 5a720f6b9f38
parent 3530 d9ca80f0759c
child 3575 4e9beacb5339
     1.1 --- a/src/Pure/drule.ML	Wed Jul 23 10:22:30 1997 +0200
     1.2 +++ b/src/Pure/drule.ML	Wed Jul 23 10:22:48 1997 +0200
     1.3 @@ -46,10 +46,12 @@
     1.4    val reflexive_thm	: thm
     1.5    val refl_implies      : thm
     1.6    val revcut_rl		: thm
     1.7 -  val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
     1.8 +  val rewrite_goal_rule	: bool * bool -> (meta_simpset -> thm -> thm option)
     1.9          -> meta_simpset -> int -> thm -> thm
    1.10    val rewrite_goals_rule: thm list -> thm -> thm
    1.11    val rewrite_rule	: thm list -> thm -> thm
    1.12 +  val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
    1.13 +	-> meta_simpset -> thm -> thm
    1.14    val RS		: thm * thm -> thm
    1.15    val RSN		: thm * (int * thm) -> thm
    1.16    val RL		: thm list * thm list -> thm list
    1.17 @@ -509,7 +511,6 @@
    1.18  
    1.19  (*** Meta-Rewriting Rules ***)
    1.20  
    1.21 -
    1.22  val reflexive_thm =
    1.23    let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
    1.24    in Thm.reflexive cx end;
    1.25 @@ -551,6 +552,8 @@
    1.26    | rewrite_rule thms th =
    1.27  	fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th;
    1.28  
    1.29 +fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
    1.30 +
    1.31  (*Rewrite the subgoals of a proof state (represented by a theorem) *)
    1.32  fun rewrite_goals_rule []   th = th
    1.33    | rewrite_goals_rule thms th =