| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 12:33:04 +0100 |
haftmann |
clarified: constructors in the sense of the code generator are not invertible;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 23:40:39 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 21:33:00 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 03 Jun 2015 19:25:05 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:53:36 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Thu, 05 Feb 2015 19:44:14 +0100 |
haftmann |
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 16:55:43 +0100 |
wenzelm |
added ML antiquotation @{apply n} or @{apply n(k)};
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 20:46:59 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Sun, 23 Mar 2014 15:46:21 +0100 |
wenzelm |
more sensible treatment of quasi-local variables (NB: Variable.add_fixes is only for term variables, while Variable.declare takes care of types within given terms);
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 10:45:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 14:32:45 +0100 |
wenzelm |
merged, resolving some conflicts;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 13:33:05 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
ported predicate compiler to 'ctr_sugar'
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 16:43:46 +0200 |
blanchet |
filled in gap in library offering
|
file |
diff |
annotate
|
| Thu, 30 May 2013 12:35:40 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:50:30 +0100 |
wenzelm |
clarified Skip_Proof.cheat_tac: more standard tactic;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 16:54:52 +0100 |
wenzelm |
just one HOLogic.Trueprop_conv, with regular exception CTERM;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2012 23:24:40 +0100 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Mon, 09 Jul 2012 09:47:59 +0200 |
bulwahn |
adding a missing entry to predicate compiler's setup
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 18:46:01 +0100 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 09:40:02 +0100 |
haftmann |
given up disfruitful branch
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 21:16:54 +0100 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Sat, 17 Dec 2011 12:10:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 21:54:32 +0100 |
wenzelm |
avoid fragile Sign.intern_const -- pass internal names directly;
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 23:05:21 +0100 |
wenzelm |
datatype dtyp with explicit sort information;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 23:30:08 +0100 |
wenzelm |
discontinued obsolete datatype "alt_names";
|
file |
diff |
annotate
|
| Fri, 11 Nov 2011 12:10:49 +0100 |
bulwahn |
using more conventional names for monad plus operations
|
file |
diff |
annotate
|
| Fri, 11 Nov 2011 08:32:45 +0100 |
bulwahn |
adding CPS compilation to predicate compiler;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Sun, 15 May 2011 18:59:27 +0200 |
wenzelm |
eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 15:03:44 +0100 |
wenzelm |
more direct use of binder_types/body_type;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:17:14 +0200 |
bulwahn |
renaming split_modeT' to split_modeT
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 18:38:59 +0200 |
bulwahn |
moving general functions from core_data to predicate_compile_aux
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:11 +0200 |
bulwahn |
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:09 +0200 |
bulwahn |
splitting large core file into core_data, mode_inference and predicate_compile_proof
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:09 +0200 |
bulwahn |
added generator_dseq compilation for a sound depth-limited compilation with small value generators
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:07 +0200 |
bulwahn |
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:06 +0200 |
bulwahn |
adding option smart_depth_limiting to predicate compiler
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 15:37:11 +0200 |
bulwahn |
applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 10:33:15 +0200 |
bulwahn |
adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 17:22:45 +0200 |
bulwahn |
removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 09:26:15 +0200 |
bulwahn |
removing clone in code_prolog and predicate_compile_quickcheck
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 09:36:39 +0200 |
bulwahn |
adding option show_invalid_clauses for a more detailed message when modes are not inferred
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 09:36:38 +0200 |
bulwahn |
proposed modes for code_pred now supports modes for mutual predicates
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 16:44:19 +0200 |
bulwahn |
handling function types more carefully than in e98a06145530
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 16:44:18 +0200 |
bulwahn |
adding order on modes
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 17:53:25 +0200 |
bulwahn |
directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:51:53 +0200 |
bulwahn |
raising an exception instead of guessing some reasonable behaviour for this function
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:19:24 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Thu, 10 Jun 2010 12:24:03 +0200 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
added switch detection to the predicate compiler
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
only add relevant predicates to the list of extra modes
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
added option for specialisation to the predicate compiler
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
|
file |
diff |
annotate
|
| Wed, 31 Mar 2010 16:44:41 +0200 |
bulwahn |
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
|
file |
diff |
annotate
|
| Wed, 31 Mar 2010 16:44:41 +0200 |
bulwahn |
adding signature to Predicate_Compile_Aux; tuning Predicate_Compile_Aux structure
|
file |
diff |
annotate
|
| Wed, 31 Mar 2010 16:44:41 +0200 |
bulwahn |
putting compilation setup of predicate compiler in a separate file
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:54 +0200 |
bulwahn |
generalized alternative functions to alternative compilation to handle arithmetic functions better
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:53 +0200 |
bulwahn |
adding registration of functions in the function flattening
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:52 +0200 |
bulwahn |
adding specialisation of predicates to the predicate compiler
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:48 +0200 |
bulwahn |
removing fishing for split thm in the predicate compiler
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:40 +0200 |
bulwahn |
removing simple equalities in introduction rules in the predicate compiler
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:36 +0200 |
bulwahn |
added new compilation to predicate_compiler
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
contextifying the compilation of the predicate compiler
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
some improvements thanks to Makarius source code review
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
adding depth_limited_random compilation to predicate compiler
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
a new simpler random compilation for the predicate compiler
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
reviving the classical depth-limited computation in the predicate compiler
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:12 +0100 |
bulwahn |
restructuring function flattening
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 21:56:55 +0100 |
wenzelm |
just one copy of structure Term_Graph (in Pure);
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 15:36:38 +0100 |
bulwahn |
adding no_topmost_reordering as new option to the code_pred command
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 13:36:15 +0100 |
bulwahn |
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 11:06:20 +0100 |
haftmann |
simplified
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:47 +0100 |
bulwahn |
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 09:11:26 +0100 |
bulwahn |
new names for predicate functions in the predicate compiler
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 09:10:42 +0100 |
bulwahn |
changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 09:10:22 +0100 |
bulwahn |
added interface of user proposals for names of generated constants
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 09:10:16 +0100 |
bulwahn |
first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 08:11:58 +0100 |
bulwahn |
adding tracing function for evaluated code; annotated compilation in the predicate compiler
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 09:55:15 +0100 |
bulwahn |
renamed rpred to random
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 12:29:02 +0100 |
bulwahn |
moved datatype mode and string functions to the auxillary structure
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 12:29:01 +0100 |
bulwahn |
improving mode parsing in the predicate compiler
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 00:07:51 +0100 |
wenzelm |
proper headers;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
added option show_modes to predicate compiler
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:02:22 +0100 |
bulwahn |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|
file |
diff |
annotate
|