src/HOLCF/domain/theorems.ML
changeset 4721 c8a8482a8124
parent 4271 3a82492e70c5
child 4755 843b5f159c7e
     1.1 --- a/src/HOLCF/domain/theorems.ML	Tue Mar 10 18:32:37 1998 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Mar 10 18:33:13 1998 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4                                  asm_simp_tac (HOLCF_ss addsimps rews) i;
     1.5  
     1.6  val chain_tac = REPEAT_DETERM o resolve_tac 
     1.7 -                [is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
     1.8 +                [chain_iterate, ch2ch_fappR, ch2ch_fappL];
     1.9  
    1.10  (* ----- general proofs ----------------------------------------------------- *)
    1.11