isabelle: src/HOL/ex/Codegenerator_Candidates.thy@14a0993fe64b (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
12b8fde1f9c0 added haftmann parents: diff changeset	16	Nat_Infinity
24433 4a405457e9d6 added explicit equation for equality of nested environments haftmann parents: 24423 diff changeset	17	Nested_Environment
26515 4a2063a8c2d2 extended haftmann parents: 26447 diff changeset	18	Option_ord
21917 12b8fde1f9c0 added haftmann parents: diff changeset	19	Permutation
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 31849 diff changeset	20	"~~/src/HOL/Number_Theory/Primes"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	21	Product_ord
35303 816e48d60b13 added Dlist haftmann parents: 33500 diff changeset	22	"~~/src/HOL/ex/Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	23	SetsAndFunctions
35617 a6528fb99641 added Table.thy haftmann parents: 35303 diff changeset	24	Table
31459 ae39b7b2a68a added trees implementing mappings haftmann parents: 31378 diff changeset	25	Tree
21917 12b8fde1f9c0 added haftmann parents: diff changeset	26	While_Combinator
12b8fde1f9c0 added haftmann parents: diff changeset	27	Word
12b8fde1f9c0 added haftmann parents: diff changeset	28	begin
12b8fde1f9c0 added haftmann parents: diff changeset	29
33500 22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	30	inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	31	empty: "sublist [] xs"
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	32	\| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	33	\| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	34
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	35	code_pred sublist .
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	36
33042 ddf1f03a9ad9 curried union as canonical list operation haftmann parents: 32479 diff changeset	37	(avoid popular infix)
ddf1f03a9ad9 curried union as canonical list operation haftmann parents: 32479 diff changeset	38	code_reserved SML upto
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	39
21917 12b8fde1f9c0 added haftmann parents: diff changeset	40	end

author	bulwahn
	Mon, 22 Mar 2010 08:30:13 +0100
changeset 35890	14a0993fe64b
parent 35617	a6528fb99641
child 36115	6601c227c5bf
permissions	-rw-r--r--