| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 22:36:09 +0200 |
blanchet |
generate proper error instead of exception if goal cannot be atomized
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:44:57 +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, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 19:57:48 +0200 |
blanchet |
ported TFL to mixture of old and new datatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
| base
|
| Tue, 19 Aug 2014 09:39:11 +0200 |
blanchet |
reduced dependency on 'Datatype' theory and ML module
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Sun, 10 Nov 2013 10:02:34 +0100 |
haftmann |
simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 22:54:42 +0200 |
blanchet |
make SMT integration slacker w.r.t. bad apples (facts)
|
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
|
| Thu, 28 Mar 2013 23:44:41 +0100 |
boehmes |
new, simpler implementation of monomorphization;
|
file |
diff |
annotate
|
| Fri, 21 Dec 2012 11:05:42 +0100 |
boehmes |
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 08:10:28 +0200 |
huffman |
move lemmas from Nat_Numeral to Int.thy and Num.thy
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 17:11:02 +0200 |
boehmes |
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 11:34:54 +0200 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Tue, 31 May 2011 19:21:20 +0200 |
boehmes |
use new monomorphizer for SMT;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2011 11:54:51 +0200 |
boehmes |
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 14:02:03 +0200 |
boehmes |
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 22:02:57 +0100 |
boehmes |
avoid ML structure aliases (especially single-letter abbreviations)
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 21:04:45 +0100 |
boehmes |
added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 08:17:23 +0100 |
boehmes |
perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 17:55:56 +0100 |
boehmes |
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 13:12:58 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 12:19:00 +0000 |
paulson |
merged
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 12:05:00 +0000 |
paulson |
made sml/nj happy
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 18:18:56 +0100 |
boehmes |
fixed trigger inference: testing if a theorem already has a trigger was too strict;
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 16:32:45 +0100 |
boehmes |
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 08:33:02 +0100 |
boehmes |
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 15:33:35 +0100 |
boehmes |
swap names for built-in tester functions (to better reflect the intuition of what they do);
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 13:31:12 +0100 |
boehmes |
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 10:39:58 +0100 |
boehmes |
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 15:45:43 +0100 |
boehmes |
share and use more utility functions;
|
file |
diff |
annotate
|
| Wed, 17 Nov 2010 08:14:56 +0100 |
boehmes |
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 12:13:44 +0100 |
boehmes |
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:10 +0200 |
boehmes |
eta-expand built-in constants; also rewrite partially applied natural number terms
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:09 +0200 |
boehmes |
optionally drop assumptions which cannot be preprocessed
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:05 +0200 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:04 +0200 |
boehmes |
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:45:12 +0200 |
boehmes |
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:39:26 +0200 |
boehmes |
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 10:52:35 +0200 |
boehmes |
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 02:29:05 +0200 |
boehmes |
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 16:29:33 +0200 |
boehmes |
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
|
file |
diff |
annotate
|
| Sat, 15 May 2010 17:59:06 +0200 |
wenzelm |
incorporated further conversions and conversionals, after some minor tuning;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:02 +0200 |
boehmes |
integrated SMT into the HOL image
|
file |
diff |
annotate
|