Tactic.norm_hhf;
authorwenzelm
Sat Jan 06 21:26:27 2001 +0100 (2001-01-06 ago)
changeset 10804306aee77eadd
parent 10803 bdc3aa1c193b
child 10805 89a29437cebc
Tactic.norm_hhf;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Jan 06 21:26:13 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Jan 06 21:26:27 2001 +0100
     1.3 @@ -266,7 +266,7 @@
     1.4    end;
     1.5  
     1.6  val rulify =
     1.7 -  standard o full_simplify [Drule.norm_hhf_eq] o
     1.8 +  standard o Tactic.norm_hhf o
     1.9    full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
    1.10    full_simplify inductive_conj;
    1.11