# HG changeset patch
# User wenzelm
# Date 973880009 -3600
# Node ID e7a8fc009d378ddcce9b85340ecbaaf1b3a5840b
# Parent  59265527d9eb29bc48805865086cd809d57a98a8
norm_hhf_tac;

diff -r 59265527d9eb -r e7a8fc009d37 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Nov 10 19:13:01 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Nov 10 19:13:29 2000 +0100
@@ -62,6 +62,7 @@
     (thm list * context attribute list) list) list -> state -> state
   val fix: (string list * string option) list -> state -> state
   val fix_i: (string list * typ option) list -> state -> state
+  val norm_hhf_tac: int -> tactic
   val hard_asm_tac: int -> tactic
   val soft_asm_tac: int -> tactic
   val assm: ProofContext.exporter
@@ -515,6 +516,10 @@
 
 (* assume *)
 
+val norm_hhf_tac = Tactic.rewrite_goal_tac [Drule.norm_hhf_eq];
+val hard_asm_tac = Tactic.etac Drule.triv_goal;
+val soft_asm_tac = Tactic.rtac Drule.triv_goal THEN' norm_hhf_tac;
+
 local
 
 fun gen_assume f exp args state =
@@ -527,13 +532,10 @@
 
 fun simple_exporter tac1 tac2 =
   (Seq.single oo Drule.implies_intr_list,
-    fn is_goal => fn n => replicate n (if is_goal then tac1 else tac2));
+    fn is_goal => fn n => replicate n (norm_hhf_tac THEN' (if is_goal then tac1 else tac2)));
 
 in
 
-val hard_asm_tac = Tactic.etac Drule.triv_goal;
-val soft_asm_tac = Tactic.rtac Drule.triv_goal;
-
 val assm = gen_assume ProofContext.assume;
 val assm_i = gen_assume ProofContext.assume_i;
 val assume = assm (simple_exporter hard_asm_tac soft_asm_tac);