equal
deleted
inserted
replaced
53 val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15); |
53 val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15); |
54 val thms = map_product |
54 val thms = map_product |
55 (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps}) |
55 (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps}) |
56 nibbles nibbles; |
56 nibbles nibbles; |
57 in |
57 in |
58 PureThy.note_thmss Thm.generated_theoremK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])] |
58 PureThy.note_thmss Thm.definitionK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])] |
59 #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms) |
59 #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms) |
60 end |
60 end |
61 *} |
61 *} |
62 |
62 |
63 lemma char_case_nibble_pair [code, code inline]: |
63 lemma char_case_nibble_pair [code, code inline]: |