equal
deleted
inserted
replaced
527 done |
527 done |
528 qed |
528 qed |
529 |
529 |
530 end |
530 end |
531 |
531 |
|
532 lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff |
|
533 lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff |
|
534 |
|
535 |
532 instantiation rat :: distrib_lattice |
536 instantiation rat :: distrib_lattice |
533 begin |
537 begin |
534 |
538 |
535 definition "(inf :: rat \<Rightarrow> rat \<Rightarrow> rat) = min" |
539 definition "(inf :: rat \<Rightarrow> rat \<Rightarrow> rat) = min" |
536 |
540 |