equal
deleted
inserted
replaced
601 |
601 |
602 syntax (xsymbols) |
602 syntax (xsymbols) |
603 "op <=" :: "['a::ord, 'a] => bool" ("op \<le>") |
603 "op <=" :: "['a::ord, 'a] => bool" ("op \<le>") |
604 "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) |
604 "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) |
605 |
605 |
606 (*Tell blast about overloading of < and <= to reduce the risk of |
|
607 its applying a rule for the wrong type*) |
|
608 ML {* |
|
609 Blast.overloaded ("op <" , domain_type); |
|
610 Blast.overloaded ("op <=", domain_type); |
|
611 *} |
|
612 |
|
613 |
606 |
614 subsubsection {* Monotonicity *} |
607 subsubsection {* Monotonicity *} |
615 |
608 |
616 locale mono = |
609 locale mono = |
617 fixes f |
610 fixes f |