isabelle: src/HOL/ex/ExecutableContent.thy@b30a342a6e29 (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
26022 b30a342a6e29 temporary adjustions haftmann parents: 25963 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
26022 b30a342a6e29 temporary adjustions haftmann parents: 25963 diff changeset	32	lemma [code func, code func del]: "(Eval.term_of \<Colon> index \<Rightarrow> term) = Eval.term_of" ..
25963 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
	Thu, 31 Jan 2008 11:47:12 +0100
changeset 26022	b30a342a6e29
parent 25963	07e08dad8a77
child 26030	4ae4ea600e8f
permissions	-rw-r--r--