changeset 16417 | 9bc16273c2d4 |
parent 15620 | 8ccdc8bc66a2 |
child 16796 | 140f1e0ea846 |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
5 |
5 |
6 header {* Binary Words *} |
6 header {* Binary Words *} |
7 |
7 |
8 theory Word |
8 theory Word |
9 imports Main |
9 imports Main |
10 files "word_setup.ML" |
10 uses "word_setup.ML" |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Auxilary Lemmas *} |
13 subsection {* Auxilary Lemmas *} |
14 |
14 |
15 lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z" |
15 lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z" |