equal
deleted
inserted
replaced
8 header {* Main Word Library *} |
8 header {* Main Word Library *} |
9 |
9 |
10 theory WordMain imports WordGenLib |
10 theory WordMain imports WordGenLib |
11 begin |
11 begin |
12 |
12 |
13 lemmas word_no_1 [simp] = word_1_no [symmetric] |
13 lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps] |
14 lemmas word_no_0 [simp] = word_0_no [symmetric] |
14 lemmas word_no_0 [simp] = word_0_no [symmetric] |
15 |
15 |
16 declare word_0_bl [simp] |
16 declare word_0_bl [simp] |
17 declare bin_to_bl_def [simp] |
17 declare bin_to_bl_def [simp] |
18 declare to_bl_0 [simp] |
18 declare to_bl_0 [simp] |