isabelle: src/HOL/Codegenerator_Test/Generate_Target_OCaml.thy@8f866fd6fae1 (annotated)

81999 513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	1	(* Author: Florian Haftmann, TU Muenchen *)
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	2
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	3	section \<open>Test of target-language specific implementations for OCaml\<close>
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	4
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	5	theory Generate_Target_OCaml
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	6	imports
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	7	"HOL-Codegenerator_Test.Generate_Target_String_Literals"
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	8	"HOL-Codegenerator_Test.Generate_Target_Bit_Operations"
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	9	begin
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	10
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	11	test_code Generate_Target_String_Literals.check in OCaml
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	12	test_code Generate_Target_Bit_Operations.check in OCaml
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	13
513f8fa74c82 more explicit tests for non-PolyML SML platforms haftmann parents: diff changeset	14	end

author	wenzelm
	Wed, 25 Jun 2025 16:35:25 +0200
changeset 82768	8f866fd6fae1
parent 81999	513f8fa74c82
permissions	-rw-r--r--