equal
deleted
inserted
replaced
78 thus "x = y" |
78 thus "x = y" |
79 proof - |
79 proof - |
80 have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False" |
80 have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False" |
81 by (auto simp add: less_acc_def split add: acc_modi.split) |
81 by (auto simp add: less_acc_def split add: acc_modi.split) |
82 with prems show ?thesis |
82 with prems show ?thesis |
83 by (unfold le_acc_def) rules |
83 by (unfold le_acc_def) iprover |
84 qed |
84 qed |
85 next |
85 next |
86 show "(x < y) = (x \<le> y \<and> x \<noteq> y)" |
86 show "(x < y) = (x \<le> y \<and> x \<noteq> y)" |
87 by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) |
87 by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) |
88 } |
88 } |