src/HOL/String.thy
changeset 38808 89ae86205739
parent 37743 0a3fa8fbcdc5
child 38858 1920158cfa17
equal deleted inserted replaced
38807:378ffc903bed 38808:89ae86205739
    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.name "nibble_pair_of_char_simps", []), [(thms, [])])]
    56   PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
    57   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    57   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    58 end
    58 end
    59 *}
    59 *}
    60 
    60 
    61 lemma char_case_nibble_pair [code, code_unfold]:
    61 lemma char_case_nibble_pair [code, code_unfold]: