src/FOLP/IFOLP.thy
changeset 45602 2a858377c3d2
parent 45594 d320f2f9f331
child 48891 c0eafbd55de3
     1.1 --- a/src/FOLP/IFOLP.thy	Sun Nov 20 17:57:09 2011 +0100
     1.2 +++ b/src/FOLP/IFOLP.thy	Sun Nov 20 20:15:02 2011 +0100
     1.3 @@ -504,7 +504,7 @@
     1.4  lemmas pred_congs = pred1_cong pred2_cong pred3_cong
     1.5  
     1.6  (*special case for the equality predicate!*)
     1.7 -lemmas eq_cong = pred2_cong [where P = "op =", standard]
     1.8 +lemmas eq_cong = pred2_cong [where P = "op ="]
     1.9  
    1.10  
    1.11  (*** Simplifications of assumed implications.