src/LCF/fix.ML
changeset 442 13ac1fd0a14d
parent 231 cb6a24451544
child 645 77474875da92
     1.1 --- a/src/LCF/fix.ML	Wed Jun 29 12:01:17 1994 +0200
     1.2 +++ b/src/LCF/fix.ML	Wed Jun 29 12:03:41 1994 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  structure Fix:FIX =
     1.5  struct
     1.6  
     1.7 -val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=u(x)::'a::cpo)"
     1.8 +val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=(u(x)::'a::cpo))"
     1.9  	(fn _ => [rewrite_goals_tac [eq_def],
    1.10  		  REPEAT(rstac[adm_conj,adm_less]1)]);
    1.11