*** empty log message ***
authornipkow
Fri Nov 27 17:01:21 1998 +0100 (1998-11-27)
changeset 59844c2fc177f4d3
parent 5983 79e301a6a51b
child 5985 9481d0cfb86e
*** empty log message ***
src/HOLCF/Fix.ML
     1.1 --- a/src/HOLCF/Fix.ML	Fri Nov 27 17:00:30 1998 +0100
     1.2 +++ b/src/HOLCF/Fix.ML	Fri Nov 27 17:01:21 1998 +0100
     1.3 @@ -686,8 +686,7 @@
     1.4          Asm_simp_tac 1,
     1.5          safe_tac HOL_cs,
     1.6          subgoal_tac "ia = i" 1,
     1.7 -        Asm_simp_tac 1,
     1.8 -        trans_tac 1
     1.9 +        ALLGOALS Asm_simp_tac
    1.10          ]);
    1.11  
    1.12    val adm_disj_lemma4 = prove_goal Nat.thy
    1.13 @@ -705,7 +704,7 @@
    1.14          Asm_simp_tac 1,
    1.15          res_inst_tac [("x","i")] exI 1,
    1.16          strip_tac 1,
    1.17 -        trans_tac 1
    1.18 +        Simp_tac 1
    1.19          ]);
    1.20  
    1.21    val adm_disj_lemma6 = prove_goal thy