changeset 3842 | b55686a7b22c |
parent 2906 | 171dedbc9bdb |
child 4089 | 96fba19bcbe2 |
--- a/src/HOL/Quot/FRACT.ML Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOL/Quot/FRACT.ML Fri Oct 10 19:02:28 1997 +0200 @@ -7,7 +7,7 @@ open FRACT; goalw thy [per_def,per_NP_def] -"(op ===)=(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"; +"(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"; fr refl; qed "inst_NP_per";