| 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
|