isabelle: src/HOL/ex/Codegenerator_Candidates.thy@d3b020134006 (annotated)

31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	1
d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	2	(* Author: Florian Haftmann, TU Muenchen *)
21917 12b8fde1f9c0 added haftmann parents: diff changeset	3
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	4	header {* A huge collection of equations to generate code from *}
21917 12b8fde1f9c0 added haftmann parents: diff changeset	5
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	6	theory Codegenerator_Candidates
21917 12b8fde1f9c0 added haftmann parents: diff changeset	7	imports
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	8	Complex_Main
21917 12b8fde1f9c0 added haftmann parents: diff changeset	9	AssocList
12b8fde1f9c0 added haftmann parents: diff changeset	10	Binomial
31849 431d8588bcad renamed theory Code_Set to Fset haftmann parents: 31807 diff changeset	11	Fset
21917 12b8fde1f9c0 added haftmann parents: diff changeset	12	Commutative_Ring
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	13	Enum
21917 12b8fde1f9c0 added haftmann parents: diff changeset	14	List_Prefix
12b8fde1f9c0 added haftmann parents: diff changeset	15	Nat_Infinity
24433 4a405457e9d6 added explicit equation for equality of nested environments haftmann parents: 24423 diff changeset	16	Nested_Environment
26515 4a2063a8c2d2 extended haftmann parents: 26447 diff changeset	17	Option_ord
21917 12b8fde1f9c0 added haftmann parents: diff changeset	18	Permutation
12b8fde1f9c0 added haftmann parents: diff changeset	19	Primes
12b8fde1f9c0 added haftmann parents: diff changeset	20	Product_ord
12b8fde1f9c0 added haftmann parents: diff changeset	21	SetsAndFunctions
31459 ae39b7b2a68a added trees implementing mappings haftmann parents: 31378 diff changeset	22	Tree
21917 12b8fde1f9c0 added haftmann parents: diff changeset	23	While_Combinator
12b8fde1f9c0 added haftmann parents: diff changeset	24	Word
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	25	"~~/src/HOL/ex/Commutative_Ring_Complete"
7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	26	"~~/src/HOL/ex/Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	27	begin
12b8fde1f9c0 added haftmann parents: diff changeset	28
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	29	(avoid popular infixes)
d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	30	code_reserved SML union inter upto
d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	31
21917 12b8fde1f9c0 added haftmann parents: diff changeset	32	end

author	paulson
	Wed, 01 Jul 2009 16:19:44 +0100
changeset 31909	d3b020134006
parent 31849	431d8588bcad
child 32479	521cc9bf2958
permissions	-rw-r--r--