equal
deleted
inserted
replaced
12 begin |
12 begin |
13 |
13 |
14 definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys" |
14 definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys" |
15 definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" |
15 definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" |
16 |
16 |
17 instance by (default, unfold less_eq_list_def less_list_def) auto |
17 instance |
|
18 by standard (auto simp: less_eq_list_def less_list_def) |
18 |
19 |
19 end |
20 end |
20 |
21 |
21 lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def] |
22 lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def] |
22 lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def] |
23 lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def] |