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

21917 12b8fde1f9c0 added haftmann parents: diff changeset	1	(* ID: $Id$
12b8fde1f9c0 added haftmann parents: diff changeset	2	Author: Florian Haftmann, TU Muenchen
12b8fde1f9c0 added haftmann parents: diff changeset	3	*)
12b8fde1f9c0 added haftmann parents: diff changeset	4
12b8fde1f9c0 added haftmann parents: diff changeset	5	header {* A huge set of executable constants *}
12b8fde1f9c0 added haftmann parents: diff changeset	6
12b8fde1f9c0 added haftmann parents: diff changeset	7	theory ExecutableContent
12b8fde1f9c0 added haftmann parents: diff changeset	8	imports
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	9	Complex_Main
21917 12b8fde1f9c0 added haftmann parents: diff changeset	10	AssocList
12b8fde1f9c0 added haftmann parents: diff changeset	11	Binomial
12b8fde1f9c0 added haftmann parents: diff changeset	12	Commutative_Ring
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	13	Enum
21917 12b8fde1f9c0 added haftmann parents: diff changeset	14	List_Prefix
12b8fde1f9c0 added haftmann parents: diff changeset	15	Nat_Infinity
24433 4a405457e9d6 added explicit equation for equality of nested environments haftmann parents: 24423 diff changeset	16	Nested_Environment
26515 4a2063a8c2d2 extended haftmann parents: 26447 diff changeset	17	Option_ord
21917 12b8fde1f9c0 added haftmann parents: diff changeset	18	Permutation
12b8fde1f9c0 added haftmann parents: diff changeset	19	Primes
12b8fde1f9c0 added haftmann parents: diff changeset	20	Product_ord
12b8fde1f9c0 added haftmann parents: diff changeset	21	SetsAndFunctions
12b8fde1f9c0 added haftmann parents: diff changeset	22	While_Combinator
12b8fde1f9c0 added haftmann parents: diff changeset	23	Word
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	24	"~~/src/HOL/ex/Commutative_Ring_Complete"
7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	25	"~~/src/HOL/ex/Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	26	begin
12b8fde1f9c0 added haftmann parents: diff changeset	27
12b8fde1f9c0 added haftmann parents: diff changeset	28	end

author	wenzelm
	Wed, 15 Oct 2008 21:45:02 +0200
changeset 28605	12d6087ec18c
parent 28229	4f06fae6a55e
child 28952	15a4b2cf8c34
permissions	-rw-r--r--