| Fri, 14 May 2010 12:01:16 +0200 |
blanchet |
produce more potential counterexamples for subset operator (cf. quantifiers)
|
changeset |
files
|
| Fri, 14 May 2010 11:24:49 +0200 |
blanchet |
improved Sledgehammer proofs
|
changeset |
files
|
| Fri, 14 May 2010 11:24:14 +0200 |
blanchet |
pass "full_type" argument to proof reconstruction
|
changeset |
files
|
| Fri, 14 May 2010 11:23:42 +0200 |
blanchet |
made Sledgehammer's full-typed proof reconstruction work for the first time;
|
changeset |
files
|
| Fri, 14 May 2010 11:20:09 +0200 |
blanchet |
delect installed ATPs dynamically, _not_ at image built time
|
changeset |
files
|
| Thu, 13 May 2010 15:09:42 +0200 |
ballarin |
Fix syntax; apparently constant apply was introduced in an earlier changeset.
|
changeset |
files
|
| Thu, 13 May 2010 14:47:15 +0200 |
ballarin |
Merged.
|
changeset |
files
|
| Thu, 13 May 2010 13:30:16 +0200 |
ballarin |
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
|
changeset |
files
|
| Thu, 13 May 2010 13:29:43 +0200 |
ballarin |
Remove improper use of mixin in class package.
|
changeset |
files
|
| Thu, 13 May 2010 14:34:05 +0200 |
nipkow |
Multiset: renamed, added and tuned lemmas;
|
changeset |
files
|
| Wed, 12 May 2010 22:33:10 -0700 |
huffman |
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
|
changeset |
files
|
| Thu, 13 May 2010 00:44:48 +0200 |
boehmes |
more precise dependencies
|
changeset |
files
|
| Wed, 12 May 2010 23:54:06 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
changeset |
files
|
| Wed, 12 May 2010 23:54:02 +0200 |
boehmes |
integrated SMT into the HOL image
|
changeset |
files
|
| Wed, 12 May 2010 23:54:01 +0200 |
boehmes |
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
|
changeset |
files
|
| Wed, 12 May 2010 23:54:00 +0200 |
boehmes |
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
|
changeset |
files
|
| Wed, 12 May 2010 23:53:59 +0200 |
boehmes |
split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
|
changeset |
files
|
| Wed, 12 May 2010 23:53:58 +0200 |
boehmes |
added tracing of reconstruction data
|
changeset |
files
|
| Wed, 12 May 2010 23:53:57 +0200 |
boehmes |
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
|
changeset |
files
|
| Wed, 12 May 2010 23:53:56 +0200 |
boehmes |
deleted SMT translation files (to be replaced by a simplified version)
|
changeset |
files
|
| Wed, 12 May 2010 23:53:55 +0200 |
boehmes |
move the addition of extra facts into a separate module
|
changeset |
files
|
| Wed, 12 May 2010 23:53:54 +0200 |
boehmes |
normalize numerals: also rewrite Numeral0 into 0
|
changeset |
files
|
| Wed, 12 May 2010 23:53:53 +0200 |
boehmes |
added missing rewrite rules for natural min and max
|
changeset |
files
|
| Wed, 12 May 2010 23:53:52 +0200 |
boehmes |
rewrite bool case expressions as if expression
|
changeset |
files
|
| Wed, 12 May 2010 23:53:51 +0200 |
boehmes |
simplified normalize_rule and moved it further down in the code
|
changeset |
files
|
| Wed, 12 May 2010 23:53:50 +0200 |
boehmes |
merged addition of rules into one function
|
changeset |
files
|
| Wed, 12 May 2010 23:53:49 +0200 |
boehmes |
added simplification for distinctness of small lists
|
changeset |
files
|
| Wed, 12 May 2010 23:53:48 +0200 |
boehmes |
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
|
changeset |
files
|
| Fri, 14 May 2010 19:53:36 +0200 |
wenzelm |
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
|
changeset |
files
|
| Thu, 13 May 2010 21:36:38 +0200 |
wenzelm |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
changeset |
files
|
| Thu, 13 May 2010 21:17:09 +0200 |
wenzelm |
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
|
changeset |
files
|
| Thu, 13 May 2010 20:15:59 +0200 |
wenzelm |
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
|
changeset |
files
|
| Thu, 13 May 2010 18:47:07 +0200 |
wenzelm |
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
|
changeset |
files
|
| Thu, 13 May 2010 18:22:10 +0200 |
wenzelm |
unconstrainT operations on proofs, according to krauss/schropp;
|
changeset |
files
|
| Thu, 13 May 2010 17:25:53 +0200 |
wenzelm |
added Proofterm.get_name variants according to krauss/schropp;
|
changeset |
files
|
| Wed, 12 May 2010 22:43:05 +0200 |
wenzelm |
conditional structure SingleAssignment;
|
changeset |
files
|
| Wed, 12 May 2010 17:10:53 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:31:43 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:27:15 +0200 |
haftmann |
tuned proofs and fact and class names
|
changeset |
files
|
| Wed, 12 May 2010 13:51:22 +0200 |
haftmann |
tuned fact collection names and some proofs
|
changeset |
files
|
| Wed, 12 May 2010 12:31:52 +0200 |
haftmann |
grouped local statements
|
changeset |
files
|
| Wed, 12 May 2010 12:31:51 +0200 |
haftmann |
tuned test problems
|
changeset |
files
|
| Wed, 12 May 2010 16:45:59 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:25:23 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:25:02 +0200 |
nipkow |
simplified proof
|
changeset |
files
|
| Wed, 12 May 2010 16:44:49 +0200 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Wed, 12 May 2010 15:25:58 +0200 |
wenzelm |
updated/unified some legacy warnings;
|
changeset |
files
|
| Wed, 12 May 2010 15:23:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 12 May 2010 14:52:23 +0200 |
wenzelm |
do not emit legacy_feature warnings here -- users have no chance to disable them;
|
changeset |
files
|
| Wed, 12 May 2010 14:17:26 +0200 |
wenzelm |
removed obsolete CVS Ids;
|
changeset |
files
|
| Wed, 12 May 2010 14:02:50 +0200 |
wenzelm |
removed some obsolete admin stuff;
|
changeset |
files
|
| Wed, 12 May 2010 14:02:19 +0200 |
wenzelm |
check NEWS;
|
changeset |
files
|
| Wed, 12 May 2010 13:54:49 +0200 |
wenzelm |
removed obsolete CVS Ids;
|
changeset |
files
|
| Wed, 12 May 2010 13:52:34 +0200 |
wenzelm |
updated some version numbers;
|
changeset |
files
|
| Wed, 12 May 2010 13:34:24 +0200 |
wenzelm |
minor tuning;
|
changeset |
files
|
| Wed, 12 May 2010 13:21:23 +0200 |
wenzelm |
reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
|
changeset |
files
|
| Wed, 12 May 2010 12:51:32 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 May 2010 12:20:16 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 12 May 2010 12:09:28 +0200 |
haftmann |
modernized specifications; tuned reification
|
changeset |
files
|
| Wed, 12 May 2010 11:18:42 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 12 May 2010 11:17:59 +0200 |
haftmann |
added lemmas concerning last, butlast, insort
|
changeset |
files
|
| Wed, 12 May 2010 11:30:18 +0200 |
Cezary Kaliszyk |
Remove RANGE_WARN
|
changeset |
files
|
| Wed, 12 May 2010 11:13:33 +0200 |
hoelzl |
clarified NEWS entry
|
changeset |
files
|
| Wed, 12 May 2010 11:08:15 +0200 |
hoelzl |
merged
|
changeset |
files
|
| Wed, 12 May 2010 11:07:46 +0200 |
hoelzl |
added NEWS entry
|
changeset |
files
|
| Tue, 11 May 2010 19:19:45 +0200 |
hoelzl |
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
|
changeset |
files
|
| Tue, 11 May 2010 19:21:39 +0200 |
hoelzl |
Add rules directly to the corresponding class locales instead.
|
changeset |
files
|
| Tue, 11 May 2010 19:21:05 +0200 |
hoelzl |
Removed usage of normalizating locales.
|
changeset |
files
|
| Tue, 11 May 2010 21:55:41 -0700 |
huffman |
speed up some proofs, fixing linarith_split_limit warnings
|
changeset |
files
|
| Tue, 11 May 2010 19:38:16 -0700 |
huffman |
fix some linarith_split_limit warnings
|
changeset |
files
|
| Tue, 11 May 2010 19:01:35 -0700 |
huffman |
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
|
changeset |
files
|
| Tue, 11 May 2010 19:00:32 -0700 |
huffman |
fix duplicate simp rule warning
|
changeset |
files
|
| Tue, 11 May 2010 18:06:58 -0700 |
huffman |
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
|
changeset |
files
|
| Tue, 11 May 2010 17:20:11 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 11 May 2010 12:38:07 -0700 |
huffman |
simplify code for emptiness check
|
changeset |
files
|
| Tue, 11 May 2010 12:05:19 -0700 |
huffman |
removed lemma real_sq_order; use power2_le_imp_le instead
|
changeset |
files
|
| Tue, 11 May 2010 21:27:09 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 11 May 2010 19:06:18 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 11 May 2010 19:00:16 +0200 |
haftmann |
represent de-Bruin indices simply by position in list
|
changeset |
files
|
| Tue, 11 May 2010 18:46:03 +0200 |
haftmann |
tuned reification functions
|
changeset |
files
|
| Tue, 11 May 2010 18:31:36 +0200 |
haftmann |
tuned code; toward a tightended interface with generated code
|
changeset |
files
|
| Tue, 11 May 2010 11:58:34 -0700 |
huffman |
fix spelling of 'superseded'
|
changeset |
files
|
| Tue, 11 May 2010 11:57:14 -0700 |
huffman |
NEWS: removed theory PReal
|
changeset |
files
|
| Tue, 11 May 2010 11:40:39 -0700 |
huffman |
collected NEWS updates for HOLCF
|
changeset |
files
|
| Tue, 11 May 2010 11:02:56 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 11 May 2010 09:10:31 -0700 |
huffman |
move floor lemmas from RealPow.thy to RComplete.thy
|
changeset |
files
|
| Tue, 11 May 2010 07:58:48 -0700 |
huffman |
add lemma tendsto_Complex
|
changeset |
files
|
| Tue, 11 May 2010 06:30:48 -0700 |
huffman |
move some theorems from RealPow.thy to Transcendental.thy
|
changeset |
files
|
| Tue, 11 May 2010 06:27:06 -0700 |
huffman |
add lemma power2_eq_1_iff; generalize some other lemmas
|
changeset |
files
|
| Mon, 10 May 2010 21:33:48 -0700 |
huffman |
minimize imports
|
changeset |
files
|
| Mon, 10 May 2010 21:27:52 -0700 |
huffman |
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
|
changeset |
files
|
| Wed, 12 May 2010 12:50:00 +0200 |
wenzelm |
clarified Pretty.font_metrics;
|
changeset |
files
|
| Wed, 12 May 2010 11:31:05 +0200 |
wenzelm |
format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking;
|
changeset |
files
|
| Wed, 12 May 2010 11:28:52 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 11 May 2010 23:36:06 +0200 |
wenzelm |
more precise pretty printing based on actual font metrics;
|
changeset |
files
|
| Tue, 11 May 2010 23:09:49 +0200 |
wenzelm |
predefined spaces;
|
changeset |
files
|
| Tue, 11 May 2010 17:55:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 11 May 2010 15:47:31 +0200 |
wenzelm |
support Isabelle plugin properties with defaults;
|
changeset |
files
|
| Tue, 11 May 2010 08:52:22 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Tue, 11 May 2010 07:45:47 +0100 |
Christian Urban |
tuned proof so that no simplifier warning is printed
|
changeset |
files
|
| Tue, 11 May 2010 08:36:02 +0200 |
haftmann |
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
|
changeset |
files
|
| Tue, 11 May 2010 08:30:02 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 11 May 2010 08:29:42 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 11 May 2010 08:29:42 +0200 |
haftmann |
theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
|
changeset |
files
|
| Mon, 10 May 2010 15:33:32 +0200 |
haftmann |
tuned; dropped strange myassoc2
|
changeset |
files
|
| Mon, 10 May 2010 15:24:43 +0200 |
haftmann |
stylized COOPER exception
|
changeset |
files
|
| Mon, 10 May 2010 15:21:13 +0200 |
haftmann |
simplified oracle
|
changeset |
files
|
| Mon, 10 May 2010 15:00:53 +0200 |
haftmann |
shorten names
|
changeset |
files
|
| Mon, 10 May 2010 14:57:04 +0200 |
haftmann |
updated references to ML files
|
changeset |
files
|
| Mon, 10 May 2010 14:55:06 +0200 |
haftmann |
only one module fpr presburger method
|
changeset |
files
|
| Mon, 10 May 2010 14:55:04 +0200 |
haftmann |
moved int induction lemma to theory Int as int_bidirectional_induct
|
changeset |
files
|
| Mon, 10 May 2010 14:18:41 +0200 |
haftmann |
tuned theory text; dropped unused lemma
|
changeset |
files
|
| Mon, 10 May 2010 14:11:50 +0200 |
haftmann |
one structure is better than three
|
changeset |
files
|
| Mon, 10 May 2010 13:58:18 +0200 |
haftmann |
less complex organization of cooper source code
|
changeset |
files
|
| Mon, 10 May 2010 12:25:49 +0200 |
haftmann |
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
|
changeset |
files
|
| Mon, 10 May 2010 14:53:33 -0700 |
huffman |
add real_mult_commute to legacy theorem names
|
changeset |
files
|
| Mon, 10 May 2010 12:12:58 -0700 |
huffman |
new construction of real numbers using Cauchy sequences
|
changeset |
files
|
| Mon, 10 May 2010 11:47:56 -0700 |
huffman |
add more credits to ex/Dedekind_Real.thy
|
changeset |
files
|
| Mon, 10 May 2010 11:30:05 -0700 |
huffman |
put construction of reals using Dedekind cuts in HOL/ex
|
changeset |
files
|
| Tue, 11 May 2010 10:36:50 +0200 |
wenzelm |
disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);
|
changeset |
files
|
| Mon, 10 May 2010 23:46:49 +0200 |
wenzelm |
simple dialogs: ensure Swing thread;
|
changeset |
files
|
| Mon, 10 May 2010 23:36:47 +0200 |
wenzelm |
font size re-adjustment according to Lobo internals;
|
changeset |
files
|
| Mon, 10 May 2010 22:29:27 +0200 |
wenzelm |
Scala for Netbeans 6.8v1.1.0rc2;
|
changeset |
files
|
| Mon, 10 May 2010 22:27:58 +0200 |
wenzelm |
more convenient get_font;
|
changeset |
files
|
| Mon, 10 May 2010 20:53:06 +0200 |
wenzelm |
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
|
changeset |
files
|
| Mon, 10 May 2010 17:37:32 +0200 |
wenzelm |
more convenient look-and-feel setup;
|
changeset |
files
|
| Mon, 10 May 2010 17:29:19 +0200 |
wenzelm |
more convenient get_font;
|
changeset |
files
|