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_Test.thy
author berghofe
Fri, 27 Nov 2009 16:26:04 +0100
changeset 33934 25d6a8982e37
parent 31378 d1cbf6393964
child 34306 e8b8ee60c1e2
permissions -rw-r--r--
Streamlined setup for monotonicity rules (no longer requires classical rules).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31378
d1cbf6393964 tuned code generator test theories
haftmann
parents: 29933
diff changeset 
     1
 












d1cbf6393964
tuned code generator test theories



haftmann


parents: 
29933

diff
changeset




     2


(* Author: Florian Haftmann, TU Muenchen *)








24195





haftmann


parents: 

diff
changeset




     3









31378






d1cbf6393964
tuned code generator test theories



haftmann


parents: 
29933

diff
changeset




     4


header {* Pervasive test of code generator using pretty literals *}








24195





haftmann


parents: 

diff
changeset




     5









31378






d1cbf6393964
tuned code generator test theories



haftmann


parents: 
29933

diff
changeset




     6


theory Codegenerator_Pretty_Test













d1cbf6393964
tuned code generator test theories



haftmann


parents: 
29933

diff
changeset




     7


imports Codegenerator_Pretty








24195





haftmann


parents: 

diff
changeset




     8


begin












haftmann


parents: 

diff
changeset




     9









25963






07e08dad8a77
distinguished examples for Efficient_Nat.thy



haftmann


parents: 
25933

diff
changeset




    10


export_code * in SML module_name CodegenTest













07e08dad8a77
distinguished examples for Efficient_Nat.thy



haftmann


parents: 
25933

diff
changeset




    11


  in OCaml module_name CodegenTest file -













07e08dad8a77
distinguished examples for Efficient_Nat.thy



haftmann


parents: 
25933

diff
changeset




    12


  in Haskell file -








25616






28d373f1482a
added div/mod examples



haftmann


parents: 
24530

diff
changeset




    13









24195





haftmann


parents: 

diff
changeset




    14


end















isabelle