isabelle: src/HOL/ex/ExecutableContent.thy@df552e6027cf (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
7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	14	Eval
21917 12b8fde1f9c0 added haftmann parents: diff changeset	15	List_Prefix
12b8fde1f9c0 added haftmann parents: diff changeset	16	Nat_Infinity
12b8fde1f9c0 added haftmann parents: diff changeset	17	NatPair
24433 4a405457e9d6 added explicit equation for equality of nested environments haftmann parents: 24423 diff changeset	18	Nested_Environment
26515 4a2063a8c2d2 extended haftmann parents: 26447 diff changeset	19	Option_ord
21917 12b8fde1f9c0 added haftmann parents: diff changeset	20	Permutation
12b8fde1f9c0 added haftmann parents: diff changeset	21	Primes
12b8fde1f9c0 added haftmann parents: diff changeset	22	Product_ord
12b8fde1f9c0 added haftmann parents: diff changeset	23	SetsAndFunctions
12b8fde1f9c0 added haftmann parents: diff changeset	24	State_Monad
12b8fde1f9c0 added haftmann parents: diff changeset	25	While_Combinator
12b8fde1f9c0 added haftmann parents: diff changeset	26	Word
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	27	"~~/src/HOL/ex/Commutative_Ring_Complete"
7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	28	"~~/src/HOL/ex/Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	29	begin
12b8fde1f9c0 added haftmann parents: diff changeset	30
26022 b30a342a6e29 temporary adjustions haftmann parents: 25963 diff changeset	31	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	32	declare fast_bv_to_nat_helper.simps [code func del]
24197 c9e3cb5e5681 proper implementation of rational numbers haftmann parents: 23690 diff changeset	33
27103 d8549f4d900b major refactorings in code generator modules haftmann parents: 26515 diff changeset	34	setup {*
d8549f4d900b major refactorings in code generator modules haftmann parents: 26515 diff changeset	35	Code.del_funcs
d8549f4d900b major refactorings in code generator modules haftmann parents: 26515 diff changeset	36	(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	37	*}
d8549f4d900b major refactorings in code generator modules haftmann parents: 26515 diff changeset	38
21917 12b8fde1f9c0 added haftmann parents: diff changeset	39	end

author	krauss
	Tue, 05 Aug 2008 14:40:48 +0200
changeset 27742	df552e6027cf
parent 27455	58b695d10cdf
child 28098	c92850d2d16c
permissions	-rw-r--r--