equal
deleted
inserted
replaced
61 apply (rule classical) |
61 apply (rule classical) |
62 apply (drule not_B1_is_B0) |
62 apply (drule not_B1_is_B0) |
63 apply (erule y) |
63 apply (erule y) |
64 done |
64 done |
65 |
65 |
66 \<comment> "simplifications for specific word lengths" |
66 \<comment> \<open>simplifications for specific word lengths\<close> |
67 lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' |
67 lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' |
68 |
68 |
69 lemmas s2n_ths = n2s_ths [symmetric] |
69 lemmas s2n_ths = n2s_ths [symmetric] |
70 |
70 |
71 lemma and_len: "xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys" |
71 lemma and_len: "xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys" |