isabelle: src/HOL/ex/ExecutableContent.thy@8764a1f1253b (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
12b8fde1f9c0 added haftmann parents: diff changeset	9	Main
25536 01753a944433 improved haftmann parents: 24626 diff changeset	10	Eval
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25572 diff changeset	11	Code_Index
23690 a5ffe85460af re-expanded paths haftmann parents: 23270 diff changeset	12	"~~/src/HOL/ex/Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	13	AssocList
12b8fde1f9c0 added haftmann parents: diff changeset	14	Binomial
12b8fde1f9c0 added haftmann parents: diff changeset	15	Commutative_Ring
23690 a5ffe85460af re-expanded paths haftmann parents: 23270 diff changeset	16	"~~/src/HOL/ex/Commutative_Ring_Complete"
24530 1bac25879117 Integrated Executable_Rat and Executable_Real theories into berghofe parents: 24433 diff changeset	17	"~~/src/HOL/Real/RealDef"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	18	GCD
12b8fde1f9c0 added haftmann parents: diff changeset	19	List_Prefix
12b8fde1f9c0 added haftmann parents: diff changeset	20	Nat_Infinity
12b8fde1f9c0 added haftmann parents: diff changeset	21	NatPair
24433 4a405457e9d6 added explicit equation for equality of nested environments haftmann parents: 24423 diff changeset	22	Nested_Environment
21917 12b8fde1f9c0 added haftmann parents: diff changeset	23	Permutation
12b8fde1f9c0 added haftmann parents: diff changeset	24	Primes
12b8fde1f9c0 added haftmann parents: diff changeset	25	Product_ord
12b8fde1f9c0 added haftmann parents: diff changeset	26	SetsAndFunctions
12b8fde1f9c0 added haftmann parents: diff changeset	27	State_Monad
12b8fde1f9c0 added haftmann parents: diff changeset	28	While_Combinator
12b8fde1f9c0 added haftmann parents: diff changeset	29	Word
12b8fde1f9c0 added haftmann parents: diff changeset	30	begin
12b8fde1f9c0 added haftmann parents: diff changeset	31
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25572 diff changeset	32	declare term_of_index.simps [code func del]
07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25572 diff changeset	33	declare fast_bv_to_nat_helper.simps [code func del]
24197 c9e3cb5e5681 proper implementation of rational numbers haftmann parents: 23690 diff changeset	34
21917 12b8fde1f9c0 added haftmann parents: diff changeset	35	end

author	haftmann
	Wed, 30 Jan 2008 10:57:44 +0100
changeset 26013	8764a1f1253b
parent 25963	07e08dad8a77
child 26022	b30a342a6e29
permissions	-rw-r--r--