equal
deleted
inserted
replaced
51 val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16; |
51 val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16; |
52 val thms = map_product |
52 val thms = map_product |
53 (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps}) |
53 (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps}) |
54 nibbles nibbles; |
54 nibbles nibbles; |
55 in |
55 in |
56 PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])] |
56 Global_Theory.note_thmss Thm.definitionK |
|
57 [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])] |
57 #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms) |
58 #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms) |
58 end |
59 end |
59 *} |
60 *} |
60 |
61 |
61 lemma char_case_nibble_pair [code, code_unfold]: |
62 lemma char_case_nibble_pair [code, code_unfold]: |