src/HOL/ex/Codegenerator_Pretty.thy
author Thomas Sewell <tsewell@nicta.com.au>
Tue, 29 Sep 2009 14:25:42 +1000
changeset 32758 cd47afaf0d78
parent 31378 d1cbf6393964
permissions -rw-r--r--
Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.


(* 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