isabelle: src/HOL/Codegenerator_Test/Generate_Abstract

75647 34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	1
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	2	(* Author: Florian Haftmann, TU Muenchen *)
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	3
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	4	section \<open>Pervasive test of code generator\<close>
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	5
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	6	theory Generate_Abstract_Char
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	7	imports
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	8	Candidates
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	9	"HOL-Library.Code_Abstract_Char"
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	10	begin
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	11
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	12	text \<open>
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	13	If any of the checks fails, inspect the code generated
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	14	by a corresponding \<open>export_code\<close> command.
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	15	\<close>
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	16
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	17	export_code _ checking SML OCaml? Haskell? Scala
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	18
34cd1d210b92 officical abstract characters for code generation haftmann parents: diff changeset	19	end

author	paulson <lp15@cam.ac.uk>
	Tue, 02 May 2023 12:51:05 +0100
changeset 77934	01c88cf514fc
parent 75647	34cd1d210b92
permissions	-rw-r--r--