isabelle: src/HOL/Codegenerator_Test/Code_Test_PolyML.thy@625bdd5c70b2 (annotated)

58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	1	(* Title: Code_Test_PolyML.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 PolyML
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_PolyML 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 PolyML
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 PolyML
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

author	blanchet
	Thu, 28 Aug 2014 00:40:37 +0200
changeset 58055	625bdd5c70b2
parent 58039	469a375212c1
child 58348	2d47c7d10b62
permissions	-rw-r--r--