isabelle: src/HOL/ex/Codegenerator_Candidates.thy@efc202e1677e (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
35303 816e48d60b13 added Dlist haftmann parents: 33500 diff changeset	11	"~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
816e48d60b13 added Dlist haftmann parents: 33500 diff changeset	12	Dlist
31849 431d8588bcad renamed theory Code_Set to Fset haftmann parents: 31807 diff changeset	13	Fset
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	14	Enum
21917 12b8fde1f9c0 added haftmann parents: diff changeset	15	List_Prefix
37023 efc202e1677e added theory More_List haftmann parents: 36962 diff changeset	16	More_List
21917 12b8fde1f9c0 added haftmann parents: diff changeset	17	Nat_Infinity
24433 4a405457e9d6 added explicit equation for equality of nested environments haftmann parents: 24423 diff changeset	18	Nested_Environment
26515 4a2063a8c2d2 extended haftmann parents: 26447 diff changeset	19	Option_ord
21917 12b8fde1f9c0 added haftmann parents: diff changeset	20	Permutation
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 31849 diff changeset	21	"~~/src/HOL/Number_Theory/Primes"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	22	Product_ord
35303 816e48d60b13 added Dlist haftmann parents: 33500 diff changeset	23	"~~/src/HOL/ex/Records"
36147 b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl haftmann parents: 36115 diff changeset	24	RBT
21917 12b8fde1f9c0 added haftmann parents: diff changeset	25	SetsAndFunctions
12b8fde1f9c0 added haftmann parents: diff changeset	26	While_Combinator
12b8fde1f9c0 added haftmann parents: diff changeset	27	begin
12b8fde1f9c0 added haftmann parents: diff changeset	28
33500 22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	29	inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	30	empty: "sublist [] xs"
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	31	\| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	32	\| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	33
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	34	code_pred sublist .
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	35
33042 ddf1f03a9ad9 curried union as canonical list operation haftmann parents: 32479 diff changeset	36	(avoid popular infix)
ddf1f03a9ad9 curried union as canonical list operation haftmann parents: 32479 diff changeset	37	code_reserved SML upto
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	38
21917 12b8fde1f9c0 added haftmann parents: diff changeset	39	end

author	haftmann
	Thu, 20 May 2010 16:35:54 +0200
changeset 37023	efc202e1677e
parent 36962	5fb251d1c32f
child 37392	b39f640b94d4
permissions	-rw-r--r--