equal
deleted
inserted
replaced
845 ord_to_filter_compat[of r0] by auto |
845 ord_to_filter_compat[of r0] by auto |
846 } |
846 } |
847 moreover |
847 moreover |
848 {assume Case2: "\<not> Well_order r0" |
848 {assume Case2: "\<not> Well_order r0" |
849 hence "?R = {}" unfolding ordLess_def by auto |
849 hence "?R = {}" unfolding ordLess_def by auto |
850 hence "wf ?R" using wf_empty by simp |
850 hence "wf ?R" by simp |
851 } |
851 } |
852 ultimately have "wf ?R" by blast |
852 ultimately have "wf ?R" by blast |
853 } |
853 } |
854 thus ?thesis by (simp add: trans_wf_iff ordLess_trans) |
854 thus ?thesis by (simp add: trans_wf_iff ordLess_trans) |
855 qed |
855 qed |