src/HOL/ex/MT.ML
changeset 22548 6ce4bddf3bcb
parent 21669 c68717c16013
     1.1 --- a/src/HOL/ex/MT.ML	Thu Mar 29 11:59:54 2007 +0200
     1.2 +++ b/src/HOL/ex/MT.ML	Thu Mar 29 14:21:45 2007 +0200
     1.3 @@ -81,11 +81,11 @@
     1.4  
     1.5  val [cih,monoh] = goal (the_context ()) "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
     1.6  by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
     1.7 -by (rtac (monoh RS monoD) 1);
     1.8 +by (rtac (monoh RS @{thm monoD}) 1);
     1.9  by (rtac (UnE RS subsetI) 1);
    1.10  by (assume_tac 1);
    1.11  by (blast_tac (claset() addSIs [cih]) 1);
    1.12 -by (rtac (monoh RS monoD RS subsetD) 1);
    1.13 +by (rtac (monoh RS @{thm monoD} RS subsetD) 1);
    1.14  by (rtac (thm "Un_upper2") 1);
    1.15  by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
    1.16  qed "gfp_coind2";