| changeset 9391 | a6ab3a442da6 |
| parent 9369 | 139fde7af7bd |
| child 9426 | d29faa6cc391 |
--- a/src/HOL/Real/PRat.ML Wed Jul 19 12:28:32 2000 +0200 +++ b/src/HOL/Real/PRat.ML Wed Jul 19 12:33:19 2000 +0200 @@ -451,7 +451,7 @@ (* lemma for proving $< is linear *) Goalw [prat_def,prat_less_def] - "ratrel ^^ {(x, y * ya)} : {p::(pnat*pnat).True}/ratrel"; + "ratrel ^^ {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel"; by (asm_full_simp_tac (simpset() addsimps [ratrel_def,quotient_def]) 1); by (Blast_tac 1); qed "lemma_prat_less_linear";