isabelle: src/HOL/Predicate_Compile.thy@844977c7abeb (annotated)

33265 01c9c6dbd890 proper headers; wenzelm parents: 33250 diff changeset	1	(* Title: HOL/Predicate_Compile.thy
01c9c6dbd890 proper headers; wenzelm parents: 33250 diff changeset	2	Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
01c9c6dbd890 proper headers; wenzelm parents: 33250 diff changeset	3	*)
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	4
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	5	header {* A compiler for predicates defined by introduction rules *}
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	6
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	7	theory Predicate_Compile
36021 c86fcf44b4c9 adopting Predicate_Compile bulwahn parents: 35898 diff changeset	8	imports New_Random_Sequence
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	9	uses
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	10	"Tools/Predicate_Compile/predicate_compile_aux.ML"
36046 c3946372f556 putting compilation setup of predicate compiler in a separate file bulwahn parents: 36032 diff changeset	11	"Tools/Predicate_Compile/predicate_compile_compilations.ML"
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	12	"Tools/Predicate_Compile/predicate_compile_core.ML"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	13	"Tools/Predicate_Compile/predicate_compile_data.ML"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	14	"Tools/Predicate_Compile/predicate_compile_fun.ML"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	15	"Tools/Predicate_Compile/predicate_compile_pred.ML"
36032 dfd30b5b4e73 adding specialisation of predicates to the predicate compiler bulwahn parents: 36021 diff changeset	16	"Tools/Predicate_Compile/predicate_compile_specialisation.ML"
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	17	"Tools/Predicate_Compile/predicate_compile.ML"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	18	begin
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	19
33265 01c9c6dbd890 proper headers; wenzelm parents: 33250 diff changeset	20	setup Predicate_Compile.setup
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	21
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33265 diff changeset	22	end

author	haftmann
	Fri, 23 Jul 2010 10:58:13 +0200
changeset 37947	844977c7abeb
parent 36046	c3946372f556
child 40052	ea46574ca815
permissions	-rw-r--r--