equal
deleted
inserted
replaced
21 "(_::'a extended) \<le> _ = False" |
21 "(_::'a extended) \<le> _ = False" |
22 |
22 |
23 case_of_simps less_eq_extended_case: less_eq_extended.simps |
23 case_of_simps less_eq_extended_case: less_eq_extended.simps |
24 |
24 |
25 definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where |
25 definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where |
26 "((x::'a extended) < y) = (x \<le> y & \<not> y \<le> x)" |
26 "((x::'a extended) < y) = (x \<le> y \<and> \<not> y \<le> x)" |
27 |
27 |
28 instance |
28 instance |
29 by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits) |
29 by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits) |
30 |
30 |
31 end |
31 end |