isabelle: src/HOL/Codegenerator_Test/Code_Test_Scala.thy@20cfa048fe7c (annotated)

59720 f893472fff31 proper headers; wenzelm parents: 58626 diff changeset	1	(* Title: HOL/Codegenerator_Test/Code_Test_Scala.thy
58039 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
58626 6c473ed0ac70 move Code_Test to HOL/Library; Andreas Lochbihler parents: 58520 diff changeset	7	theory Code_Test_Scala imports "../Library/Code_Test" begin
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	8
58520 a4d1f8041af0 accomplish potentially case-insenstive file systems for Scala haftmann parents: 58348 diff changeset	9	declare [[scala_case_insensitive]]
a4d1f8041af0 accomplish potentially case-insenstive file systems for Scala haftmann parents: 58348 diff changeset	10
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	11	test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	12
58348 2d47c7d10b62 add target language evaluators for the value command; Andreas Lochbihler parents: 58039 diff changeset	13	value [Scala] "14 + 7 * -12 :: integer"
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	14
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	15	end

author	wenzelm
	Fri, 07 Aug 2015 16:15:53 +0200
changeset 60864	20cfa048fe7c
parent 59720	f893472fff31
child 61856	4b1b85f38944
permissions	-rw-r--r--