isabelle: src/HOL/Codegenerator_Test/Candidates.thy@2b561e7a0512 (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
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37407 diff changeset	6	theory Candidates
21917 12b8fde1f9c0 added haftmann parents: diff changeset	7	imports
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	8	Complex_Main
51160 599ff65b85e2 systematic conversions between nat and nibble/char; haftmann parents: 49077 diff changeset	9	"~~/src/HOL/Library/Library"
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	10	"~~/src/HOL/Library/Sublist_Order"
51173 3cbb4e95a565 Sieve of Eratosthenes haftmann parents: 51161 diff changeset	11	"~~/src/HOL/Number_Theory/Eratosthenes"
35303 816e48d60b13 added Dlist haftmann parents: 33500 diff changeset	12	"~~/src/HOL/ex/Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	13	begin
12b8fde1f9c0 added haftmann parents: diff changeset	14
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	15	inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	16	where
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	17	empty: "sublist [] xs"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	18	\| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	19	\| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
33500 22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	20
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	21	code_pred sublist .
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	22
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	23	code_reserved SML upto -- {* avoid popular infix *}
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	24
21917 12b8fde1f9c0 added haftmann parents: diff changeset	25	end

author	blanchet
	Sat, 12 Jul 2014 11:31:22 +0200
changeset 57546	2b561e7a0512
parent 51173	3cbb4e95a565
child 58678	398e05aa84d4
permissions	-rw-r--r--