unified rewrite/rewrite_cterm/simplify interface;
authorwenzelm
Sun Oct 14 22:05:46 2001 +0200 (2001-10-14)
changeset 1176848bc55f43774
parent 11767 7380c9d45626
child 11769 1fcf1eb51608
unified rewrite/rewrite_cterm/simplify interface;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Sun Oct 14 22:05:01 2001 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sun Oct 14 22:05:46 2001 +0200
     1.3 @@ -83,8 +83,9 @@
     1.4    val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
     1.5    val resolve_tac       : thm list -> int -> tactic
     1.6    val res_inst_tac      : (string*string)list -> thm -> int -> tactic
     1.7 -  val full_rewrite      : thm list -> cterm -> thm
     1.8 -  val full_rewrite_cterm : thm list -> cterm -> cterm
     1.9 +  val rewrite           : bool -> thm list -> cterm -> thm
    1.10 +  val rewrite_cterm     : bool -> thm list -> cterm -> cterm
    1.11 +  val simplify          : bool -> thm list -> thm -> thm
    1.12    val rewrite_goal_tac  : thm list -> int -> tactic
    1.13    val rewrite_goals_rule: thm list -> thm -> thm
    1.14    val rewrite_rule      : thm list -> thm -> thm
    1.15 @@ -487,9 +488,10 @@
    1.16  val simple_prover =
    1.17    result1 (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
    1.18  
    1.19 -val full_rewrite = MetaSimplifier.full_rewrite_aux simple_prover;
    1.20 -val full_rewrite_cterm = (#2 o Thm.dest_comb o #prop o Thm.crep_thm) oo full_rewrite;
    1.21 -val rewrite_rule = MetaSimplifier.rewrite_rule_aux simple_prover;
    1.22 +val rewrite = MetaSimplifier.rewrite_aux simple_prover;
    1.23 +val rewrite_cterm = (#2 o Thm.dest_comb o #prop o Thm.crep_thm) ooo rewrite;
    1.24 +val simplify = MetaSimplifier.simplify_aux simple_prover;
    1.25 +val rewrite_rule = simplify true;
    1.26  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    1.27  
    1.28  (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)