src/HOL/Predicate_Compile.thy
Mon, 17 Feb 2014 17:49:29 +0100 wenzelm more informative error;
Thu, 16 May 2013 10:08:28 +0200 Andreas Lochbihler setup for set membership as a predicate for code_pred
Thu, 14 Feb 2013 15:27:10 +0100 haftmann reform of predicate compiler / quickcheck theories:
Mon, 12 Nov 2012 23:24:40 +0100 haftmann tuned import order
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch
Thu, 23 Feb 2012 21:25:59 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 11 Nov 2011 08:32:45 +0100 bulwahn adding CPS compilation to predicate compiler;
Thu, 21 Oct 2010 19:13:09 +0200 bulwahn splitting large core file into core_data, mode_inference and predicate_compile_proof
Wed, 31 Mar 2010 16:44:41 +0200 bulwahn putting compilation setup of predicate compiler in a separate file
Mon, 29 Mar 2010 17:30:52 +0200 bulwahn adding specialisation of predicates to the predicate compiler
Mon, 29 Mar 2010 17:30:39 +0200 bulwahn adopting Predicate_Compile
Mon, 22 Mar 2010 20:58:52 +0100 wenzelm recovered header;
Mon, 22 Mar 2010 08:30:13 +0100 bulwahn removed unused Predicate_Compile_Set
Mon, 22 Mar 2010 08:30:13 +0100 bulwahn reviving the classical depth-limited computation in the predicate compiler
Wed, 20 Jan 2010 11:56:45 +0100 bulwahn refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
Wed, 28 Oct 2009 00:07:51 +0100 wenzelm proper headers;
Tue, 27 Oct 2009 09:02:22 +0100 bulwahn including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
less more (0) tip