| Thu, 27 May 2010 12:03:59 +0200 |
wenzelm |
more reactive message handling, notably for follow_caret mode;
|
changeset |
files
|
| Thu, 27 May 2010 00:47:15 +0200 |
wenzelm |
Command.toString: include id for debugging;
|
changeset |
files
|
| Wed, 26 May 2010 18:19:36 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 26 May 2010 18:19:12 +0200 |
wenzelm |
refer to polyml-5.3.0-old for ppc-darwin;
|
changeset |
files
|
| Wed, 26 May 2010 17:52:32 +0200 |
boehmes |
try logical and theory abstraction before full abstraction (avoids warnings of linarith)
|
changeset |
files
|
| Wed, 26 May 2010 15:35:17 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Wed, 26 May 2010 15:34:47 +0200 |
boehmes |
hide constants and types introduced by SMT,
|
changeset |
files
|
| Wed, 26 May 2010 11:59:06 +0200 |
haftmann |
more convenient order of code equations
|
changeset |
files
|
| Wed, 26 May 2010 11:34:23 +0200 |
wenzelm |
misc updates for release;
|
changeset |
files
|
| Tue, 25 May 2010 23:03:13 +0200 |
wenzelm |
eliminated obsolete priority message from Isabelle_Process protocol;
|
changeset |
files
|
| Tue, 25 May 2010 22:21:31 +0200 |
wenzelm |
moved ML files where they are actually used;
|
changeset |
files
|
| Tue, 25 May 2010 22:12:26 +0200 |
wenzelm |
renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;
|
changeset |
files
|
| Tue, 25 May 2010 21:49:44 +0200 |
wenzelm |
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
|
changeset |
files
|
| Tue, 25 May 2010 20:28:16 +0200 |
wenzelm |
eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
|
changeset |
files
|
| Tue, 25 May 2010 20:22:55 +0200 |
wenzelm |
tuned -- avoid catch-all exception pattern;
|
changeset |
files
|
| Tue, 25 May 2010 11:13:49 +0200 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Tue, 25 May 2010 10:57:02 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 24 May 2010 21:19:25 +0100 |
webertj |
merged
|
changeset |
files
|
| Mon, 24 May 2010 21:18:22 +0100 |
webertj |
Typo fixed.
|
changeset |
files
|
| Mon, 24 May 2010 12:42:17 -0700 |
huffman |
move HOLCF/Sum_Cpo.thy to HOLCF/Library
|
changeset |
files
|
| Mon, 24 May 2010 12:10:24 -0700 |
huffman |
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
|
changeset |
files
|
| Mon, 24 May 2010 11:29:49 -0700 |
huffman |
move unused pattern match syntax stuff into HOLCF/ex
|
changeset |
files
|
| Mon, 24 May 2010 09:32:52 -0700 |
huffman |
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
|
changeset |
files
|
| Mon, 24 May 2010 13:48:57 +0200 |
haftmann |
more lemmas
|
changeset |
files
|
| Mon, 24 May 2010 13:48:56 +0200 |
haftmann |
induction and case rules
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Store registrations in efficient data structure.
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Avoid recomputation of registration instance for lookup.
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Consistently use equality for registration lookup.
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Cleaner implementation of sublocale command.
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Reapply mixin patch: base for performance improvements.
|
changeset |
files
|
| Sun, 23 May 2010 19:30:29 -0700 |
huffman |
merged
|
changeset |
files
|
| Sun, 23 May 2010 19:30:14 -0700 |
huffman |
declare a few more cont2cont rules
|
changeset |
files
|
| Sat, 22 May 2010 19:17:18 -0700 |
huffman |
HOLCF no longer redefines 'consts' command
|
changeset |
files
|
| Sat, 22 May 2010 18:34:38 -0700 |
huffman |
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
|
changeset |
files
|
| Sat, 22 May 2010 17:57:16 -0700 |
huffman |
simplify fixrec continuity tactic
|
changeset |
files
|
| Sun, 23 May 2010 22:56:45 +0200 |
krauss |
used sledgehammer[isar_proof] to replace slow metis call
|
changeset |
files
|
| Sun, 23 May 2010 17:23:18 +0100 |
webertj |
Typo fixed.
|
changeset |
files
|
| Sun, 23 May 2010 17:22:30 +0100 |
webertj |
Typo fixed.
|
changeset |
files
|
| Sun, 23 May 2010 14:56:58 +0100 |
webertj |
Minor proof tuning.
|
changeset |
files
|
| Sun, 23 May 2010 13:00:01 +0100 |
webertj |
Improved document structure.
|
changeset |
files
|
| Sun, 23 May 2010 10:55:01 +0100 |
webertj |
Minor proof tuning.
|
changeset |
files
|
| Sun, 23 May 2010 10:38:11 +0100 |
webertj |
merged
|
changeset |
files
|
| Sun, 23 May 2010 10:37:43 +0100 |
webertj |
Refactoring, minor extensions (e.g., church_rosser).
|
changeset |
files
|
| Sat, 22 May 2010 17:44:12 -0700 |
huffman |
NEWS: removed fixrec_simp attribute
|
changeset |
files
|
| Sat, 22 May 2010 16:46:18 -0700 |
huffman |
merged
|
changeset |
files
|
| Sat, 22 May 2010 16:45:46 -0700 |
huffman |
disambiguate some syntax
|
changeset |
files
|
| Sat, 22 May 2010 14:04:05 -0700 |
huffman |
optimize continuity proofs in fixrec package, using cont2cont rules
|
changeset |
files
|
| Sat, 22 May 2010 13:40:15 -0700 |
huffman |
add beta_cfun simproc, which uses cont2cont rules
|
changeset |
files
|
| Sat, 22 May 2010 13:27:36 -0700 |
huffman |
removed fixrec_simp attribute (cf. a2a1c8a658ef)
|
changeset |
files
|
| Sat, 22 May 2010 12:56:33 -0700 |
huffman |
simplify definition of eta_tac
|
changeset |
files
|
| Sat, 22 May 2010 12:36:50 -0700 |
huffman |
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
|
changeset |
files
|
| Sat, 22 May 2010 10:02:07 -0700 |
huffman |
remove cont2cont simproc; instead declare cont2cont rules as simp rules
|
changeset |
files
|
| Sat, 22 May 2010 08:30:40 -0700 |
huffman |
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
|
changeset |
files
|
| Sat, 22 May 2010 11:01:59 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sat, 22 May 2010 10:13:02 +0200 |
haftmann |
modernized sorting algorithms; quicksort implements sort
|
changeset |
files
|
| Sat, 22 May 2010 10:12:50 +0200 |
haftmann |
modernized sorting algorithms; quicksort implements sort
|
changeset |
files
|
| Sat, 22 May 2010 10:12:49 +0200 |
haftmann |
localized properties_for_sort
|
changeset |
files
|
| Mon, 24 May 2010 23:19:40 +0200 |
wenzelm |
@tailrec annotation;
|
changeset |
files
|
| Mon, 24 May 2010 23:01:51 +0200 |
wenzelm |
renamed "rev" to "reverse" following usual Scala conventions;
|
changeset |
files
|
| Sat, 22 May 2010 23:59:09 +0200 |
wenzelm |
parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;
|
changeset |
files
|
| Sat, 22 May 2010 23:53:09 +0200 |
wenzelm |
added rev_iterator;
|
changeset |
files
|
| Sat, 22 May 2010 22:30:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 22 May 2010 22:30:37 +0200 |
wenzelm |
access statically typed dockable windows;
|
changeset |
files
|
| Sat, 22 May 2010 22:05:41 +0200 |
wenzelm |
simplified dockables using class Dockable;
|
changeset |
files
|
| Sat, 22 May 2010 21:48:01 +0200 |
wenzelm |
generic dockable window;
|
changeset |
files
|
| Sat, 22 May 2010 20:59:55 +0200 |
wenzelm |
separate event bus and dockable for raw output (stdout);
|
changeset |
files
|
| Sat, 22 May 2010 20:37:59 +0200 |
wenzelm |
more Mac OS problems;
|
changeset |
files
|
| Sat, 22 May 2010 20:37:20 +0200 |
wenzelm |
ignore system messages;
|
changeset |
files
|
| Sat, 22 May 2010 20:20:51 +0200 |
wenzelm |
use proper ISABELLE_PLATFORM instead of adhoc uname;
|
changeset |
files
|
| Sat, 22 May 2010 20:10:11 +0200 |
wenzelm |
refrain from using bold within the term language -- looks odd in Lobo with error/warning background;
|
changeset |
files
|
| Sat, 22 May 2010 20:02:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 22 May 2010 20:00:28 +0200 |
wenzelm |
removed timing;
|
changeset |
files
|
| Sat, 22 May 2010 19:42:20 +0200 |
wenzelm |
rendering information and style sheets via settings;
|
changeset |
files
|
| Fri, 21 May 2010 23:48:48 +0200 |
wenzelm |
more brackets -- unaligned to prevent odd auto-indentation;
|
changeset |
files
|
| Fri, 21 May 2010 23:21:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 21 May 2010 17:16:16 +0200 |
haftmann |
adjusted to changes in Mapping.thy
|
changeset |
files
|
| Fri, 21 May 2010 15:28:25 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 21 May 2010 15:22:37 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 21 May 2010 15:22:37 +0200 |
haftmann |
more lemmas about mappings, in particular keys
|
changeset |
files
|
| Fri, 21 May 2010 15:22:36 +0200 |
haftmann |
refined
|
changeset |
files
|
| Fri, 21 May 2010 11:50:34 +0200 |
haftmann |
nats in Haskell are readable
|
changeset |
files
|
| Fri, 21 May 2010 10:40:59 +0200 |
Cezary Kaliszyk |
Let rsp and prs in fun_rel/fun_map format
|
changeset |
files
|
| Fri, 21 May 2010 23:19:27 +0200 |
wenzelm |
tuned zoom_box;
|
changeset |
files
|
| Fri, 21 May 2010 22:08:13 +0200 |
wenzelm |
print calculation result in the context where the fact is actually defined -- proper externing;
|
changeset |
files
|
| Fri, 21 May 2010 21:28:31 +0200 |
wenzelm |
future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);
|
changeset |
files
|
| Fri, 21 May 2010 20:46:00 +0200 |
wenzelm |
some message styling;
|
changeset |
files
|
| Fri, 21 May 2010 20:10:45 +0200 |
wenzelm |
simplified message markup, using plain XML.Elem directly;
|
changeset |
files
|
| Fri, 21 May 2010 18:10:19 +0200 |
wenzelm |
more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
|
changeset |
files
|
| Fri, 21 May 2010 17:26:42 +0200 |
wenzelm |
refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
|
changeset |
files
|
| Fri, 21 May 2010 16:49:33 +0200 |
wenzelm |
bad_result: report fully explicit message;
|
changeset |
files
|
| Fri, 21 May 2010 16:40:25 +0200 |
wenzelm |
observe additional isabelle-jedit.css for component and user;
|
changeset |
files
|
| Fri, 21 May 2010 15:29:20 +0200 |
wenzelm |
added checkboxes for debug/tracing filter;
|
changeset |
files
|
| Fri, 21 May 2010 14:53:19 +0200 |
wenzelm |
more abstract view on prover output messages;
|
changeset |
files
|
| Fri, 21 May 2010 12:59:44 +0200 |
wenzelm |
added some tooltips;
|
changeset |
files
|
| Fri, 21 May 2010 11:51:03 +0200 |
wenzelm |
HTML_Panel.handler as overridable method;
|
changeset |
files
|
| Fri, 21 May 2010 11:50:19 +0200 |
wenzelm |
added Library.undefined (in Scala);
|
changeset |
files
|
| Fri, 21 May 2010 11:16:01 +0200 |
wenzelm |
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
|
changeset |
files
|
| Fri, 21 May 2010 11:12:54 +0200 |
wenzelm |
component resize: full handle_resize;
|
changeset |
files
|
| Thu, 20 May 2010 21:19:38 -0700 |
huffman |
speed up some proofs and fix some warnings
|
changeset |
files
|
| Thu, 20 May 2010 23:22:37 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 20 May 2010 19:55:42 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 20 May 2010 18:00:48 +0200 |
haftmann |
proper code generator for complement
|
changeset |
files
|
| Thu, 20 May 2010 17:35:02 +0200 |
haftmann |
proper document text
|
changeset |
files
|
| Thu, 20 May 2010 17:29:43 +0200 |
haftmann |
implement Mapping.map_entry
|
changeset |
files
|
| Thu, 20 May 2010 17:29:43 +0200 |
haftmann |
operations default, map_entry, map_default; more lemmas
|
changeset |
files
|
| Thu, 20 May 2010 16:43:00 +0200 |
haftmann |
added More_List.thy explicitly
|
changeset |
files
|
| Thu, 20 May 2010 16:40:29 +0200 |
haftmann |
renamed List_Set to the now more appropriate More_Set
|
changeset |
files
|
| Thu, 20 May 2010 16:35:54 +0200 |
haftmann |
added theory More_List
|
changeset |
files
|
| Thu, 20 May 2010 16:35:53 +0200 |
haftmann |
moved generic List operations to theory More_List
|
changeset |
files
|
| Thu, 20 May 2010 16:35:53 +0200 |
haftmann |
adjusted
|
changeset |
files
|
| Thu, 20 May 2010 16:35:52 +0200 |
haftmann |
turned old-style mem into an input abbreviation
|
changeset |
files
|
| Thu, 20 May 2010 23:20:01 +0200 |
wenzelm |
zoom font size;
|
changeset |
files
|
| Thu, 20 May 2010 23:19:28 +0200 |
wenzelm |
added somewhat generic zoom box;
|
changeset |
files
|
| Thu, 20 May 2010 21:32:48 +0200 |
wenzelm |
try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
|
changeset |
files
|
| Thu, 20 May 2010 21:10:03 +0200 |
wenzelm |
mutate displayed document synchronously in Swing thread, for improved robustness;
|
changeset |
files
|
| Thu, 20 May 2010 21:07:05 +0200 |
wenzelm |
read style sheets only once;
|
changeset |
files
|
| Thu, 20 May 2010 20:56:26 +0200 |
wenzelm |
handle component resize for output / HTML panel;
|
changeset |
files
|
| Thu, 20 May 2010 20:22:00 +0200 |
wenzelm |
Isabelle_System: allow explicit isabelle_home argument;
|
changeset |
files
|
| Thu, 20 May 2010 20:20:52 +0200 |
wenzelm |
enable shell script editor mode;
|
changeset |
files
|
| Thu, 20 May 2010 16:25:22 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 20 May 2010 07:36:50 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Thu, 20 May 2010 07:34:45 +0200 |
bulwahn |
deactivated timing of infering modes
|
changeset |
files
|
| Wed, 19 May 2010 18:24:09 +0200 |
bulwahn |
adapting examples
|
changeset |
files
|
| Wed, 19 May 2010 18:24:09 +0200 |
bulwahn |
changing operations for accessing data to work with contexts
|
changeset |
files
|
| Wed, 19 May 2010 18:24:08 +0200 |
bulwahn |
removed unnecessary Thm.transfer in the predicate compiler
|
changeset |
files
|
| Wed, 19 May 2010 18:24:07 +0200 |
bulwahn |
changing compilation to work only with contexts; adapting quickcheck
|
changeset |
files
|
| Wed, 19 May 2010 18:24:06 +0200 |
bulwahn |
removing unused argument in print_modes function
|
changeset |
files
|
| Wed, 19 May 2010 18:24:05 +0200 |
bulwahn |
moving towards working with proof contexts in the predicate compiler
|
changeset |
files
|
| Wed, 19 May 2010 18:24:04 +0200 |
bulwahn |
improved values command to handle a special case with tuples and polymorphic predicates more correctly
|
changeset |
files
|
| Wed, 19 May 2010 18:24:03 +0200 |
bulwahn |
improved behaviour of defined_functions in the predicate compiler
|
changeset |
files
|
| Wed, 19 May 2010 17:01:07 -0700 |
huffman |
move some example files into new HOLCF/Tutorial directory
|
changeset |
files
|
| Wed, 19 May 2010 16:28:24 -0700 |
huffman |
remove redundant hdvd relation
|
changeset |
files
|
| Wed, 19 May 2010 16:08:41 -0700 |
huffman |
remove unnecessary constant Fixrec.bind
|
changeset |
files
|
| Wed, 19 May 2010 14:38:25 -0700 |
huffman |
add section about fixrec definitions with looping simp rules
|
changeset |
files
|
| Wed, 19 May 2010 13:07:15 -0700 |
huffman |
more informative error message for fixrec when continuity proof fails
|
changeset |
files
|
| Thu, 20 May 2010 16:22:50 +0200 |
wenzelm |
determine margin just before rendering -- proper reformatting when updating;
|
changeset |
files
|
| Thu, 20 May 2010 15:51:28 +0200 |
wenzelm |
simplified alignment via FlowPanel;
|
changeset |
files
|
| Thu, 20 May 2010 13:54:31 +0200 |
wenzelm |
more systematic treatment of physical document wrt. font size etc.;
|
changeset |
files
|
| 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
|
| 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
|