isabelle: src/HOL/ex/ExecutableContent.thy@d8549f4d900b (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
26447 fef9dde61a46 added Enum haftmann parents: 26030 diff changeset	11	Enum
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25572 diff changeset	12	Code_Index
26030 4ae4ea600e8f fixed record problem haftmann parents: 26022 diff changeset	13	"~~/src/HOL/ex/Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	14	AssocList
12b8fde1f9c0 added haftmann parents: diff changeset	15	Binomial
12b8fde1f9c0 added haftmann parents: diff changeset	16	Commutative_Ring
23690 a5ffe85460af re-expanded paths haftmann parents: 23270 diff changeset	17	"~~/src/HOL/ex/Commutative_Ring_Complete"
24530 1bac25879117 Integrated Executable_Rat and Executable_Real theories into berghofe parents: 24433 diff changeset	18	"~~/src/HOL/Real/RealDef"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	19	GCD
12b8fde1f9c0 added haftmann parents: diff changeset	20	List_Prefix
12b8fde1f9c0 added haftmann parents: diff changeset	21	Nat_Infinity
12b8fde1f9c0 added haftmann parents: diff changeset	22	NatPair
24433 4a405457e9d6 added explicit equation for equality of nested environments haftmann parents: 24423 diff changeset	23	Nested_Environment
26515 4a2063a8c2d2 extended haftmann parents: 26447 diff changeset	24	Option_ord
21917 12b8fde1f9c0 added haftmann parents: diff changeset	25	Permutation
12b8fde1f9c0 added haftmann parents: diff changeset	26	Primes
12b8fde1f9c0 added haftmann parents: diff changeset	27	Product_ord
12b8fde1f9c0 added haftmann parents: diff changeset	28	SetsAndFunctions
12b8fde1f9c0 added haftmann parents: diff changeset	29	State_Monad
12b8fde1f9c0 added haftmann parents: diff changeset	30	While_Combinator
12b8fde1f9c0 added haftmann parents: diff changeset	31	Word
12b8fde1f9c0 added haftmann parents: diff changeset	32	begin
12b8fde1f9c0 added haftmann parents: diff changeset	33
26022 b30a342a6e29 temporary adjustions haftmann parents: 25963 diff changeset	34	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	35	declare fast_bv_to_nat_helper.simps [code func del]
24197 c9e3cb5e5681 proper implementation of rational numbers haftmann parents: 23690 diff changeset	36
27103 d8549f4d900b major refactorings in code generator modules haftmann parents: 26515 diff changeset	37	setup {*
d8549f4d900b major refactorings in code generator modules haftmann parents: 26515 diff changeset	38	Code.del_funcs
d8549f4d900b major refactorings in code generator modules haftmann parents: 26515 diff changeset	39	(AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "env"}))
d8549f4d900b major refactorings in code generator modules haftmann parents: 26515 diff changeset	40	*}
d8549f4d900b major refactorings in code generator modules haftmann parents: 26515 diff changeset	41
21917 12b8fde1f9c0 added haftmann parents: diff changeset	42	end

author	haftmann
	Tue, 10 Jun 2008 15:30:06 +0200
changeset 27103	d8549f4d900b
parent 26515	4a2063a8c2d2
child 27421	7e458bd56860
permissions	-rw-r--r--