isabelle: src/HOL/Codegenerator_Test/Candidates.thy@0a8adca22974 (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
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37407 diff changeset	9	Library
49077 154f25a162e3 renamed theory List_Prefix into Sublist (since it is not only about prefixes) Christian Sternagel parents: 41884 diff changeset	10	"~~/src/HOL/Library/Sublist"
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 31849 diff changeset	11	"~~/src/HOL/Number_Theory/Primes"
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
33500 22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	15	inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	16	empty: "sublist [] xs"
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	17	\| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	18	\| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	19
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	20	code_pred sublist .
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	21
33042 ddf1f03a9ad9 curried union as canonical list operation haftmann parents: 32479 diff changeset	22	(avoid popular infix)
ddf1f03a9ad9 curried union as canonical list operation haftmann parents: 32479 diff changeset	23	code_reserved SML upto
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	24
21917 12b8fde1f9c0 added haftmann parents: diff changeset	25	end

author	hoelzl
	Wed, 10 Oct 2012 12:12:24 +0200
changeset 49785	0a8adca22974
parent 49077	154f25a162e3
child 51160	599ff65b85e2
permissions	-rw-r--r--