# HG changeset patch # User nipkow # Date 912182481 -3600 # Node ID 4c2fc177f4d33513bef084eb51da3414e2aee142 # Parent 79e301a6a51bbbce2fe8329f895feeec28782216 *** empty log message *** diff -r 79e301a6a51b -r 4c2fc177f4d3 src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Fri Nov 27 17:00:30 1998 +0100 +++ b/src/HOLCF/Fix.ML Fri Nov 27 17:01:21 1998 +0100 @@ -686,8 +686,7 @@ Asm_simp_tac 1, safe_tac HOL_cs, subgoal_tac "ia = i" 1, - Asm_simp_tac 1, - trans_tac 1 + ALLGOALS Asm_simp_tac ]); val adm_disj_lemma4 = prove_goal Nat.thy @@ -705,7 +704,7 @@ Asm_simp_tac 1, res_inst_tac [("x","i")] exI 1, strip_tac 1, - trans_tac 1 + Simp_tac 1 ]); val adm_disj_lemma6 = prove_goal thy