# 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);