src/HOL/Codegenerator_Test/Candidates_Pretty.thy
changeset 51160 599ff65b85e2
parent 51143 0a2371e7ced3
equal deleted inserted replaced
51159:3fe7242f8346 51160:599ff65b85e2
     2 (* Author: Florian Haftmann, TU Muenchen *)
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     3 
     4 header {* Generating code using pretty literals and natural number literals  *}
     4 header {* Generating code using pretty literals and natural number literals  *}
     5 
     5 
     6 theory Candidates_Pretty
     6 theory Candidates_Pretty
     7 imports Candidates Code_Char_ord Code_Target_Numeral
     7 imports Candidates Code_Char Code_Target_Numeral
     8 begin
     8 begin
     9 
     9 
    10 end
    10 end