| Thu, 20 May 2010 11:44:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 20 May 2010 11:36:30 +0200 |
wenzelm |
general Isabelle_System.try_read;
|
changeset |
files
|
| Thu, 20 May 2010 10:43:46 +0200 |
wenzelm |
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
|
changeset |
files
|
| Thu, 20 May 2010 10:31:20 +0200 |
wenzelm |
inverted "Freeze" to "Follow", which is the default;
|
changeset |
files
|
| Wed, 19 May 2010 21:18:02 +0200 |
wenzelm |
basic controls to freeze/update prover results;
|
changeset |
files
|
| Wed, 19 May 2010 18:05:34 +0200 |
wenzelm |
show fully detailed protocol messages;
|
changeset |
files
|
| Wed, 19 May 2010 17:39:22 +0200 |
wenzelm |
some updates following src/Tools/jEdit/dist-template/settings;
|
changeset |
files
|
| Wed, 19 May 2010 12:35:20 +0200 |
haftmann |
spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
|
changeset |
files
|
| Wed, 19 May 2010 10:17:31 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 19 May 2010 10:17:05 +0200 |
haftmann |
dropped legacy_unconstrainT
|
changeset |
files
|
| Wed, 19 May 2010 10:14:37 +0200 |
haftmann |
new version of triv_of_class machinery without legacy_unconstrain
|
changeset |
files
|
| Wed, 19 May 2010 09:21:30 +0200 |
haftmann |
merge
|
changeset |
files
|
| Wed, 19 May 2010 09:20:36 +0200 |
haftmann |
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
|
changeset |
files
|
| Tue, 18 May 2010 19:00:55 -0700 |
huffman |
remove several redundant lemmas about floor and ceiling
|
changeset |
files
|
| Tue, 18 May 2010 06:28:42 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 17 May 2010 18:59:59 -0700 |
huffman |
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
|
changeset |
files
|
| Mon, 17 May 2010 18:51:25 -0700 |
huffman |
simplify proof
|
changeset |
files
|
| Mon, 17 May 2010 16:52:34 -0700 |
huffman |
simplify proof
|
changeset |
files
|
| Mon, 17 May 2010 15:58:32 -0700 |
huffman |
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
|
changeset |
files
|
| Tue, 18 May 2010 10:13:33 +0200 |
wenzelm |
prefer structure Keyword and Parse;
|
changeset |
files
|
| Tue, 18 May 2010 00:01:51 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 17 May 2010 12:00:10 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 17 May 2010 08:45:46 -0700 |
huffman |
remove simp attribute from square_eq_1_iff
|
changeset |
files
|
| Mon, 17 May 2010 17:50:09 +0200 |
blanchet |
merged
|
changeset |
files
|
| Mon, 17 May 2010 15:21:11 +0200 |
blanchet |
make sure chained facts don't pop up in the metis proof
|
changeset |
files
|
| Mon, 17 May 2010 12:15:37 +0200 |
blanchet |
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
|
changeset |
files
|
| Mon, 17 May 2010 10:18:14 +0200 |
blanchet |
generate proper arity declarations for TFrees for SPASS's DFG format;
|
changeset |
files
|
| Mon, 17 May 2010 10:16:54 +0200 |
blanchet |
identify common SPASS error more clearly
|
changeset |
files
|
| Mon, 17 May 2010 08:40:17 -0700 |
huffman |
remove simp attribute from power2_eq_1_iff
|
changeset |
files
|
| Mon, 17 May 2010 10:58:58 +0200 |
haftmann |
dropped old Library/Word.thy and toy example ex/Adder.thy
|
changeset |
files
|
| Mon, 17 May 2010 10:58:31 +0200 |
haftmann |
dropped old Library/Word.thy and toy example ex/Adder.thy
|
changeset |
files
|
| Tue, 18 May 2010 00:01:03 +0200 |
wenzelm |
do not open Legacy by default;
|
changeset |
files
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
changeset |
files
|
| Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
changeset |
files
|
| Mon, 17 May 2010 15:05:32 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 17 May 2010 15:02:44 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 17 May 2010 14:23:54 +0200 |
wenzelm |
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
|
changeset |
files
|
| Mon, 17 May 2010 10:20:55 +0200 |
wenzelm |
centralized legacy aliases;
|
changeset |
files
|
| Sun, 16 May 2010 00:02:11 +0200 |
wenzelm |
prefer structure Parse_Spec;
|
changeset |
files
|
| Sat, 15 May 2010 23:40:00 +0200 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
changeset |
files
|
| Sat, 15 May 2010 23:32:15 +0200 |
wenzelm |
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
|
changeset |
files
|
| Sat, 15 May 2010 23:23:45 +0200 |
wenzelm |
renamed structure ValueParse to Parse_Value;
|
changeset |
files
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
changeset |
files
|
| Sat, 15 May 2010 22:24:25 +0200 |
wenzelm |
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
|
changeset |
files
|
| Sat, 15 May 2010 22:15:57 +0200 |
wenzelm |
renamed Outer_Parse to Parse (in Scala);
|
changeset |
files
|
| Sat, 15 May 2010 22:05:49 +0200 |
wenzelm |
renamed Outer_Keyword to Keyword (in Scala);
|
changeset |
files
|
| Sat, 15 May 2010 21:57:27 +0200 |
wenzelm |
avoid open Conv;
|
changeset |
files
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
changeset |
files
|
| Sat, 15 May 2010 21:41:32 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
changeset |
files
|
| Sat, 15 May 2010 21:09:54 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 May 2010 18:29:18 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 15 May 2010 07:48:24 -0700 |
huffman |
add real_le_linear to list of legacy theorem names
|
changeset |
files
|
| Sat, 15 May 2010 16:20:54 +0200 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Sat, 15 May 2010 18:15:50 +0200 |
wenzelm |
removed unused conversions;
|
changeset |
files
|
| Sat, 15 May 2010 18:12:58 +0200 |
wenzelm |
tuned header;
|
changeset |
files
|
| Sat, 15 May 2010 18:11:00 +0200 |
wenzelm |
moved normarith.ML where it is actually used;
|
changeset |
files
|
| Sat, 15 May 2010 17:59:06 +0200 |
wenzelm |
incorporated further conversions and conversionals, after some minor tuning;
|
changeset |
files
|
| Sat, 15 May 2010 15:31:33 +0200 |
wenzelm |
eliminated redundant runtime checks;
|
changeset |
files
|
| Sat, 15 May 2010 00:45:42 +0200 |
krauss |
normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
|
changeset |
files
|
| Sat, 15 May 2010 15:07:39 +0200 |
wenzelm |
more precise dependencies for HOL-Word-SMT_Examples;
|
changeset |
files
|
| Sat, 15 May 2010 13:31:25 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 14 May 2010 23:35:35 +0200 |
blanchet |
merge
|
changeset |
files
|
| Fri, 14 May 2010 23:34:24 +0200 |
blanchet |
added Sledgehammer documentation to TOC
|
changeset |
files
|
| Fri, 14 May 2010 23:32:48 +0200 |
blanchet |
added some Sledgehammer news
|
changeset |
files
|
| Fri, 14 May 2010 23:16:33 +0200 |
blanchet |
document Nitpick changes
|
changeset |
files
|
| Fri, 14 May 2010 22:43:24 +0200 |
blanchet |
merge
|
changeset |
files
|
| Fri, 14 May 2010 22:43:00 +0200 |
blanchet |
added Sledgehammer manual;
|
changeset |
files
|
| Fri, 14 May 2010 22:30:24 +0200 |
blanchet |
renamed Sledgehammer options
|
changeset |
files
|
| Fri, 14 May 2010 22:29:50 +0200 |
blanchet |
renamed options
|
changeset |
files
|
| Fri, 14 May 2010 22:28:39 +0200 |
blanchet |
remove support for crashing beta solver HaifaSat
|
changeset |
files
|
| Fri, 14 May 2010 16:15:10 +0200 |
blanchet |
renamed two Sledgehammer options
|
changeset |
files
|
| Fri, 14 May 2010 22:46:58 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 14 May 2010 22:46:41 +0200 |
nipkow |
added listsum lemmas
|
changeset |
files
|
| Fri, 14 May 2010 21:23:29 +0200 |
ballarin |
Revert mixin patch due to inacceptable performance drop.
|
changeset |
files
|
| Fri, 14 May 2010 15:27:07 +0200 |
blanchet |
add "no_atp"s to Nitpick lemmas
|
changeset |
files
|
| Fri, 14 May 2010 15:26:26 +0200 |
blanchet |
query _HOME environment variables at run-time, not at build-time
|
changeset |
files
|
| Fri, 14 May 2010 15:09:37 +0200 |
blanchet |
move Refute dependency from Plain to Main
|
changeset |
files
|
| Fri, 14 May 2010 15:07:53 +0200 |
blanchet |
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
|
changeset |
files
|
| Fri, 14 May 2010 15:02:38 +0200 |
blanchet |
recognize new Kodkod error message syntax
|
changeset |
files
|
| Fri, 14 May 2010 14:14:22 +0200 |
blanchet |
improve precision of set constructs in Nitpick
|
changeset |
files
|
| 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
|