isabelle: src/HOL/ex/Codegenerator_Candidates.thy@3282c12a856c (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
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 31849 diff changeset	19	"~~/src/HOL/Number_Theory/Primes"
21917 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	Thomas Sewell <tsewell@nicta.com.au>
	Fri, 11 Sep 2009 20:58:29 +1000
changeset 32749	3282c12a856c
parent 32479	521cc9bf2958
child 33042	ddf1f03a9ad9
permissions	-rw-r--r--