isabelle: src/HOL/Codegenerator_Test/Candidates.thy@d02b01e5ab8f (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
41884 335895ffbd94 modernized imports; wenzelm parents: 37695 diff changeset	10	"~~/src/HOL/Library/List_Prefix"
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	huffman
	Wed, 24 Aug 2011 11:56:57 -0700
changeset 44514	d02b01e5ab8f
parent 41884	335895ffbd94
child 49077	154f25a162e3
permissions	-rw-r--r--