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/Codegenerator_Test/Code_Test_Scala.thy
author blanchet
Wed, 03 Sep 2014 00:06:24 +0200
changeset 58152 6fe60a9a5bad
parent 58039 469a375212c1
child 58348 2d47c7d10b62
permissions -rw-r--r--
use 'datatype_new' in 'Main'
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset 
     1
 
(*  Title:      Code_Test_Scala.thy
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset 
     2
 
    Author:     Andreas Lochbihler, ETH Zurich
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset 
     3
 












469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     4


Test case for test_code on Scala













469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     5


*)













469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     6














469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     7


theory Code_Test_Scala imports Code_Test begin 













469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     8














469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




     9


test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala













469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




    10














469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




    11


eval_term "14 + 7 * -12 :: integer" in Scala













469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




    12














469a375212c1
add testing framework for generated code



Andreas Lochbihler


parents: 

diff
changeset




    13


end















isabelle