isabelle: src/HOL/Predicate_Compile.thy@14a0993fe64b (annotated)

35879 99818df5b8f5 reviving the classical depth-limited computation in the predicate compiler bulwahn parents: 34948 diff changeset	1
33265 01c9c6dbd890 proper headers; wenzelm parents: 33250 diff changeset	2	(* Title: HOL/Predicate_Compile.thy
01c9c6dbd890 proper headers; wenzelm parents: 33250 diff changeset	3	Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
01c9c6dbd890 proper headers; wenzelm parents: 33250 diff changeset	4	*)
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	5
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	6	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	7
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	8	theory Predicate_Compile
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33265 diff changeset	9	imports Random_Sequence Quickcheck
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	10	uses
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	11	"Tools/Predicate_Compile/predicate_compile_aux.ML"
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"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	16	"Tools/Predicate_Compile/predicate_compile.ML"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	17	begin
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	18
33265 01c9c6dbd890 proper headers; wenzelm parents: 33250 diff changeset	19	setup Predicate_Compile.setup
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: diff changeset	20
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33265 diff changeset	21	end

author	bulwahn
	Mon, 22 Mar 2010 08:30:13 +0100
changeset 35890	14a0993fe64b
parent 35879	99818df5b8f5
child 35898	c890a3835d15
permissions	-rw-r--r--