equal
deleted
inserted
replaced
449 by (Fast_tac 1); |
449 by (Fast_tac 1); |
450 qed "qless_Ex"; |
450 qed "qless_Ex"; |
451 |
451 |
452 (* lemma for proving $< is linear *) |
452 (* lemma for proving $< is linear *) |
453 Goalw [prat_def,prat_less_def] |
453 Goalw [prat_def,prat_less_def] |
454 "ratrel ^^ {(x, y * ya)} : {p::(pnat*pnat).True}/ratrel"; |
454 "ratrel ^^ {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel"; |
455 by (asm_full_simp_tac (simpset() addsimps [ratrel_def,quotient_def]) 1); |
455 by (asm_full_simp_tac (simpset() addsimps [ratrel_def,quotient_def]) 1); |
456 by (Blast_tac 1); |
456 by (Blast_tac 1); |
457 qed "lemma_prat_less_linear"; |
457 qed "lemma_prat_less_linear"; |
458 |
458 |
459 (* linearity of < -- Gleason p. 120 - Proposition 9-2.6 *) |
459 (* linearity of < -- Gleason p. 120 - Proposition 9-2.6 *) |