src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
Fri, 11 Nov 2011 10:40:36 +0100 bulwahn increasing values_timeout to avoid failures of isatest with HOL-IMP
Fri, 11 Nov 2011 08:32:45 +0100 bulwahn adding CPS compilation to predicate compiler;
Thu, 20 Oct 2011 09:11:13 +0200 bulwahn modernizing predicate_compile_quickcheck
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Sat, 23 Jul 2011 17:22:28 +0200 wenzelm explicit structure ML_System;
Tue, 19 Jul 2011 00:07:21 +0200 krauss values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations
Fri, 01 Jul 2011 15:16:03 +0200 wenzelm proper @{binding} antiquotations (relevant for formal references);
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Wed, 08 Jun 2011 00:01:20 +0200 krauss removed generation of instantiated pattern set, which is never actually used
Wed, 01 Jun 2011 08:07:28 +0200 bulwahn creating a free variable with proper name and local mixfix syntax (cf. db9b9e46131c)
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Wed, 27 Apr 2011 19:39:50 +0200 wenzelm some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Mon, 28 Mar 2011 10:25:28 +0200 bulwahn changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ
Thu, 24 Mar 2011 15:29:31 +0100 bulwahn allowing special set comprehensions in values command; adding an example for special set comprehension in values
Wed, 23 Mar 2011 08:50:31 +0100 bulwahn making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
Sun, 20 Mar 2011 21:20:07 +0100 wenzelm pervasive cond_timeit;
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Wed, 01 Dec 2010 15:35:40 +0100 wenzelm just one HOLogic.mk_comp;
Wed, 01 Dec 2010 13:09:08 +0100 wenzelm just one Term.dest_funT;
Tue, 02 Nov 2010 20:55:12 +0100 wenzelm simplified some time constants;
Mon, 25 Oct 2010 21:17:14 +0200 bulwahn renaming split_modeT' to split_modeT
Mon, 25 Oct 2010 21:17:13 +0200 bulwahn options as first argument to check functions
Mon, 25 Oct 2010 21:17:10 +0200 bulwahn adding a global time limit to the values command
Fri, 22 Oct 2010 18:38:59 +0200 bulwahn adding generator quickcheck
Fri, 22 Oct 2010 18:38:59 +0200 bulwahn restructuring values command and adding generator compilation
Thu, 21 Oct 2010 19:13:10 +0200 bulwahn using a signature in core_data and moving some more functions to core_data
Thu, 21 Oct 2010 19:13:09 +0200 bulwahn splitting large core file into core_data, mode_inference and predicate_compile_proof
Thu, 21 Oct 2010 19:13:09 +0200 bulwahn added generator_dseq compilation for a sound depth-limited compilation with small value generators
Thu, 21 Oct 2010 19:13:08 +0200 bulwahn for now safely but unpractically assume no predicate is terminating
Thu, 21 Oct 2010 19:13:07 +0200 bulwahn adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
Wed, 29 Sep 2010 10:33:15 +0200 bulwahn improving the compilation to handle predicate arguments in higher-order argument positions
Wed, 29 Sep 2010 10:33:14 +0200 bulwahn putting the last step of the proof in a TRY block to handle the case that the simplifier already solved the goal
Tue, 28 Sep 2010 13:44:06 +0200 bulwahn merged
Tue, 28 Sep 2010 11:59:58 +0200 bulwahn using SUBPROOF to ensure that rewriting is not done on the further subgoals of proof
Tue, 28 Sep 2010 11:59:57 +0200 bulwahn avoiding instable rotate_tac and using the nice Subgoal.FOCUS_PREMS instead
Tue, 28 Sep 2010 11:59:52 +0200 bulwahn only modes but not types are used to destruct terms and types; this allows to interpret arguments that are predicates simply as input
Tue, 28 Sep 2010 11:59:51 +0200 bulwahn weakening check for higher-order relations, but adding check for consistent modes
Tue, 28 Sep 2010 11:59:51 +0200 bulwahn handling higher-order relations in output terms; improving proof procedure; added test case
Tue, 28 Sep 2010 11:59:50 +0200 bulwahn renaming use_random to use_generators in the predicate compiler
Tue, 28 Sep 2010 11:59:48 +0200 bulwahn fixed a typo that caused the preference of non-random modes to be ignored
Tue, 28 Sep 2010 12:34:41 +0200 krauss consolidated tupled_lambda; moved to structure HOLogic
Fri, 24 Sep 2010 15:30:30 +0200 wenzelm actually handle Type.TYPE_MATCH, not arbitrary exceptions;
Fri, 24 Sep 2010 08:12:10 +0200 bulwahn being a little less strict than in 2e06dad03dd3
Thu, 23 Sep 2010 17:22:45 +0200 bulwahn removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned
Thu, 23 Sep 2010 17:22:44 +0200 bulwahn moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule
Thu, 23 Sep 2010 14:50:16 +0200 bulwahn handling TYPE_MATCH error by raising user error message if user gives introduction rules with mismatching types
Thu, 23 Sep 2010 14:50:16 +0200 bulwahn improving naming of assumptions in code_pred
Thu, 23 Sep 2010 14:50:15 +0200 bulwahn adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
Thu, 23 Sep 2010 14:50:14 +0200 bulwahn removing duplicate rewrite rule from simpset in predicate compiler
Thu, 23 Sep 2010 14:50:13 +0200 bulwahn rewriting function mk_Eval_of in predicate compiler
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Mon, 20 Sep 2010 09:26:20 +0200 bulwahn code_pred_intro can be used to name facts for the code_pred command
Thu, 16 Sep 2010 17:51:16 +0200 haftmann merged
Thu, 16 Sep 2010 16:51:33 +0200 haftmann adjusted to changes in Code_Runtime
Thu, 16 Sep 2010 13:49:04 +0200 bulwahn adding mode inference to prolog compilation; separate between (ad-hoc) code modifications and system_configuration; adapting quickcheck
Wed, 15 Sep 2010 15:40:35 +0200 haftmann Code_Runtime.value, corresponding to ML_Context.value
Wed, 15 Sep 2010 15:31:32 +0200 haftmann code_eval renamed to code_runtime
Wed, 15 Sep 2010 12:16:08 +0200 haftmann merged
Wed, 15 Sep 2010 11:30:32 +0200 haftmann replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
less more (0) -100 -60 tip