src/HOL/ex/Codegenerator_Pretty.thy
author wenzelm
Sun, 20 Dec 2009 15:42:12 +0100
changeset 34139 d1ded303fe0e
parent 31378 d1cbf6393964
permissions -rw-r--r--
Outer lexical syntax for Isabelle/Isar -- Scala version.


(* Author: Florian Haftmann, TU Muenchen *)

header {* Generating code using pretty literals and natural number literals  *}

theory Codegenerator_Pretty
imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat
begin

declare isnorm.simps [code del]

end