Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Codegenerator_Pretty.thy
author wenzelm
Tue, 21 Jul 2009 01:03:18 +0200
changeset 32091 30e2ffbba718
parent 31378 d1cbf6393964
permissions -rw-r--r--
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24195
haftmann
parents:
diff changeset 
     1
 







31378






d1cbf6393964
tuned code generator test theories



haftmann


parents: 
29933

diff
changeset




     2


(* Author: Florian Haftmann, TU Muenchen *)













d1cbf6393964
tuned code generator test theories



haftmann


parents: 
29933

diff
changeset




     3














d1cbf6393964
tuned code generator test theories



haftmann


parents: 
29933

diff
changeset




     4


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








24195





haftmann


parents: 

diff
changeset




     5













haftmann


parents: 

diff
changeset




     6


theory Codegenerator_Pretty








31378






d1cbf6393964
tuned code generator test theories



haftmann


parents: 
29933

diff
changeset




     7


imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat








24195





haftmann


parents: 

diff
changeset




     8


begin












haftmann


parents: 

diff
changeset




     9









28562






4e74209f113e
`code func` now just `code`



haftmann


parents: 
28335

diff
changeset




    10


declare isnorm.simps [code del]








28228






7ebe8dc06cbb
evaluation using code generator



haftmann


parents: 
26468

diff
changeset




    11









24195





haftmann


parents: 

diff
changeset




    12


end















isabelle