isabelle: src/HOL/ex/Codegenerator_Candidates.thy@89d1903fbd50 (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
21917 12b8fde1f9c0 added haftmann parents: diff changeset	25	While_Combinator
12b8fde1f9c0 added haftmann parents: diff changeset	26	Word
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	wenzelm
	Wed, 14 Apr 2010 22:07:01 +0200
changeset 36135	89d1903fbd50
parent 36115	6601c227c5bf
child 36147	b43b22f63665
permissions	-rw-r--r--