isabelle: src/HOL/ex/ExecutableContent.thy@cd3f37ba3e25 (annotated)

28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28229 diff changeset	1	(* Author: Florian Haftmann, TU Muenchen
21917 12b8fde1f9c0 added haftmann parents: diff changeset	2	*)
12b8fde1f9c0 added haftmann parents: diff changeset	3
12b8fde1f9c0 added haftmann parents: diff changeset	4	header {* A huge set of executable constants *}
12b8fde1f9c0 added haftmann parents: diff changeset	5
12b8fde1f9c0 added haftmann parents: diff changeset	6	theory ExecutableContent
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
12b8fde1f9c0 added haftmann parents: diff changeset	11	Commutative_Ring
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	12	Enum
21917 12b8fde1f9c0 added haftmann parents: diff changeset	13	List_Prefix
12b8fde1f9c0 added haftmann parents: diff changeset	14	Nat_Infinity
24433 4a405457e9d6 added explicit equation for equality of nested environments haftmann parents: 24423 diff changeset	15	Nested_Environment
26515 4a2063a8c2d2 extended haftmann parents: 26447 diff changeset	16	Option_ord
21917 12b8fde1f9c0 added haftmann parents: diff changeset	17	Permutation
12b8fde1f9c0 added haftmann parents: diff changeset	18	Primes
12b8fde1f9c0 added haftmann parents: diff changeset	19	Product_ord
12b8fde1f9c0 added haftmann parents: diff changeset	20	SetsAndFunctions
12b8fde1f9c0 added haftmann parents: diff changeset	21	While_Combinator
12b8fde1f9c0 added haftmann parents: diff changeset	22	Word
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	23	"~~/src/HOL/ex/Commutative_Ring_Complete"
7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	24	"~~/src/HOL/ex/Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	25	begin
12b8fde1f9c0 added haftmann parents: diff changeset	26
29125 d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs krauss parents: 28952 diff changeset	27	text {* However, some aren't executable *}
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs krauss parents: 28952 diff changeset	28
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs krauss parents: 28952 diff changeset	29	declare pair_leq_def[code del]
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs krauss parents: 28952 diff changeset	30	declare max_weak_def[code del]
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs krauss parents: 28952 diff changeset	31	declare min_weak_def[code del]
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs krauss parents: 28952 diff changeset	32	declare ms_weak_def[code del]
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs krauss parents: 28952 diff changeset	33
21917 12b8fde1f9c0 added haftmann parents: diff changeset	34	end

author	wenzelm
	Thu, 26 Feb 2009 22:13:01 +0100
changeset 30127	cd3f37ba3e25
parent 29125	d41182a8135c
child 30328	ab47f43f7581
permissions	-rw-r--r--