src/Pure/tactic.ML
changeset 15696 1da4ce092c0b
parent 15671 8df681866dc9
child 15797 a63605582573
     1.1 --- a/src/Pure/tactic.ML	Mon Apr 11 12:18:27 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Mon Apr 11 12:34:34 2005 +0200
     1.3 @@ -70,6 +70,7 @@
     1.4    val net_biresolve_tac : (bool*thm) list -> int -> tactic
     1.5    val net_match_tac     : thm list -> int -> tactic
     1.6    val net_resolve_tac   : thm list -> int -> tactic
     1.7 +  val norm_hhf_plain    : thm -> thm
     1.8    val norm_hhf_rule     : thm -> thm
     1.9    val norm_hhf_tac      : int -> tactic
    1.10    val prune_params_tac  : tactic
    1.11 @@ -532,9 +533,12 @@
    1.12  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
    1.13  fun rewtac def = rewrite_goals_tac [def];
    1.14  
    1.15 +fun norm_hhf_plain th =
    1.16 +  if Drule.is_norm_hhf (prop_of th) then th
    1.17 +  else rewrite_rule [Drule.norm_hhf_eq] th;
    1.18 +
    1.19  fun norm_hhf_rule th =
    1.20 - (if Drule.is_norm_hhf (prop_of th) then th
    1.21 -  else rewrite_rule [Drule.norm_hhf_eq] th) |> Drule.gen_all;
    1.22 +  th |> norm_hhf_plain |> Drule.gen_all;
    1.23  
    1.24  val norm_hhf_tac =
    1.25    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)