| Wed, 11 Sep 2013 11:34:27 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Wed, 11 Sep 2013 11:08:48 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 11 Sep 2013 11:07:39 +0200 |
wenzelm |
updated for release;
|
changeset |
files
|
| Wed, 11 Sep 2013 00:00:59 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 10 Sep 2013 23:50:03 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 10 Sep 2013 23:08:48 +0200 |
wenzelm |
updated to jedit_build-20130910 (with update of jedit.jar and Highlight.jar);
|
changeset |
files
|
| Tue, 10 Sep 2013 22:37:01 +0200 |
wenzelm |
disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;
|
changeset |
files
|
| Tue, 10 Sep 2013 18:14:47 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 10 Sep 2013 16:09:33 +0200 |
wenzelm |
discontinued obsolete command-line tool "isabelle build_dialog";
|
changeset |
files
|
| Wed, 11 Sep 2013 10:57:09 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Wed, 11 Sep 2013 09:51:30 +0200 |
blanchet |
speed up often-called function
|
changeset |
files
|
| Wed, 11 Sep 2013 09:51:19 +0200 |
blanchet |
got rid of currently unused data structure, to speed up relevance filter
|
changeset |
files
|
| Wed, 11 Sep 2013 09:50:48 +0200 |
blanchet |
adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
|
changeset |
files
|
| Tue, 10 Sep 2013 16:02:02 +0200 |
blanchet |
sorted out dependencies
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:52 +0200 |
blanchet |
faster detection of tautologies
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
slight speed optimization
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
got rid of another slowdown factor in relevance filter
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
removed completely needless, inefficient code
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
minor speed optimization
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
avoid double traversal of term
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
got rid of old, needless logic
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
moved ML function closer to its remaining use
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
faster uniquification
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
stronger fact normalization
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
gracefully handle huge thys
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
speed up detection of simp rules
|
changeset |
files
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
don't be so verbose about SMT solver failures
|
changeset |
files
|
| Tue, 10 Sep 2013 14:02:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 10 Sep 2013 11:57:53 +0200 |
wenzelm |
more portable hash-bang;
|
changeset |
files
|
| Tue, 10 Sep 2013 11:46:51 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 10 Sep 2013 00:22:12 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 10 Sep 2013 00:18:30 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 09 Sep 2013 23:11:02 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 09 Sep 2013 23:55:35 +0200 |
blanchet |
make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices
|
changeset |
files
|
| Mon, 09 Sep 2013 23:54:59 +0200 |
blanchet |
since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion
|
changeset |
files
|
| Mon, 09 Sep 2013 23:09:37 +0200 |
blanchet |
more docs
|
changeset |
files
|
| Mon, 09 Sep 2013 20:24:15 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 09 Sep 2013 17:28:08 +0200 |
wenzelm |
proper apple.awt.application.name for Java 7;
|
changeset |
files
|
| Mon, 09 Sep 2013 17:02:06 +0200 |
wenzelm |
generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
|
changeset |
files
|
| Mon, 09 Sep 2013 16:15:48 +0200 |
wenzelm |
more robust Mac OS X application support;
|
changeset |
files
|
| Mon, 09 Sep 2013 15:53:02 +0200 |
wenzelm |
use polyml-5.5.1 (SVN), to increase chances of stability of this test;
|
changeset |
files
|
| Mon, 09 Sep 2013 14:48:16 +0200 |
wenzelm |
override potential changes in $ISABELLE_HOME_USER/etc/settings;
|
changeset |
files
|
| Mon, 09 Sep 2013 14:22:39 +0200 |
wenzelm |
generate application ini based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
|
changeset |
files
|
| Mon, 09 Sep 2013 13:48:06 +0200 |
wenzelm |
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
|
changeset |
files
|
| Mon, 09 Sep 2013 18:14:54 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 09 Sep 2013 18:12:41 +0200 |
blanchet |
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
|
changeset |
files
|
| Mon, 09 Sep 2013 15:22:04 +0200 |
blanchet |
limit the number of instances of a single theorem
|
changeset |
files
|
| Mon, 09 Sep 2013 15:22:04 +0200 |
blanchet |
move metis to new monomorphizer
|
changeset |
files
|
| Mon, 09 Sep 2013 15:22:04 +0200 |
blanchet |
use new monomorphizer in Sledgehammer
|
changeset |
files
|
| Mon, 09 Sep 2013 14:23:04 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 09 Sep 2013 14:22:11 +0200 |
blanchet |
include map theorems in datastructure for "primcorec"
|
changeset |
files
|
| Mon, 09 Sep 2013 13:47:58 +0200 |
blanchet |
enriched data structure with necessary theorems
|
changeset |
files
|
| Sun, 08 Sep 2013 19:25:06 +0200 |
wenzelm |
updated exe -- more explicit icon;
|
changeset |
files
|
| Sun, 08 Sep 2013 18:37:42 +0200 |
wenzelm |
more official lib/logo/isabelle.bmp;
|
changeset |
files
|
| Sun, 08 Sep 2013 18:10:12 +0200 |
wenzelm |
use windows_app based on WinRun4J;
|
changeset |
files
|
| Sun, 08 Sep 2013 17:51:56 +0200 |
wenzelm |
updated to WinRun4J;
|
changeset |
files
|
| Sun, 08 Sep 2013 12:26:07 +0200 |
traytel |
tuned whitespace
|
changeset |
files
|
| Sun, 08 Sep 2013 12:26:05 +0200 |
traytel |
don't register "sequential" as a keyword for now as this breaks the parser for function
|
changeset |
files
|
| Sat, 07 Sep 2013 23:09:26 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sat, 07 Sep 2013 20:12:38 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 07 Sep 2013 19:45:36 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sat, 07 Sep 2013 19:18:05 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sat, 07 Sep 2013 18:37:25 +0200 |
wenzelm |
imitate "isabelle java" and "isabelle jedit" wrt. classpath and options (see also a221a4fdb5a0);
|
changeset |
files
|
| Sat, 07 Sep 2013 18:24:24 +0200 |
wenzelm |
generate application wrapper for Linux;
|
changeset |
files
|
| Sat, 07 Sep 2013 17:43:13 +0200 |
wenzelm |
observe "stopped" after Cygwin init (which is itself uninterruptible);
|
changeset |
files
|
| Sat, 07 Sep 2013 17:32:55 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sat, 07 Sep 2013 17:23:05 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 07 Sep 2013 17:11:44 +0200 |
wenzelm |
Cygwin_Init based on System_Dialog;
|
changeset |
files
|
| Sat, 07 Sep 2013 16:33:10 +0200 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Sat, 07 Sep 2013 15:28:16 +0200 |
wenzelm |
more robust exit;
|
changeset |
files
|
| Sat, 07 Sep 2013 15:10:33 +0200 |
wenzelm |
Build_Dialog based on System_Dialog;
|
changeset |
files
|
| Sat, 07 Sep 2013 14:14:25 +0200 |
wenzelm |
clarified close operations;
|
changeset |
files
|
| Sat, 07 Sep 2013 14:07:12 +0200 |
wenzelm |
clarified result;
|
changeset |
files
|
| Sat, 07 Sep 2013 13:59:47 +0200 |
wenzelm |
dialog for system processes, with optional output window;
|
changeset |
files
|
| Sat, 07 Sep 2013 11:36:03 +0200 |
wenzelm |
more portable access to icon -- avoid Isabelle_System which is not yet initialized in bootstrap;
|
changeset |
files
|
| Sat, 07 Sep 2013 11:28:30 +0200 |
wenzelm |
odd workaround for scalac to enable nohup;
|
changeset |
files
|
| Sat, 07 Sep 2013 11:02:27 +0200 |
wenzelm |
odd workaround for scalac to enable nohup;
|
changeset |
files
|
| Sat, 07 Sep 2013 00:02:19 +0200 |
wenzelm |
build session before start of jedit;
|
changeset |
files
|
| Fri, 06 Sep 2013 22:28:28 +0200 |
wenzelm |
imitate "isabelle java" and "isabelle jedit" wrt. classpath and options;
|
changeset |
files
|
| Fri, 06 Sep 2013 22:07:26 +0200 |
wenzelm |
more Proof General legacy;
|
changeset |
files
|
| Fri, 06 Sep 2013 21:28:07 +0200 |
wenzelm |
use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);
|
changeset |
files
|
| Fri, 06 Sep 2013 21:13:19 +0200 |
wenzelm |
warm start of Isabelle/jEdit from Isabelle/Scala;
|
changeset |
files
|
| Fri, 06 Sep 2013 18:15:25 +0200 |
wenzelm |
prefer explicit thread;
|
changeset |
files
|
| Fri, 06 Sep 2013 18:14:50 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 06 Sep 2013 17:55:01 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 06 Sep 2013 17:26:58 +0200 |
wenzelm |
prefer Isabelle/Scala over bash;
|
changeset |
files
|
| Fri, 06 Sep 2013 17:20:48 +0200 |
wenzelm |
prefer Isabelle/Scala over bash;
|
changeset |
files
|
| Fri, 06 Sep 2013 17:01:49 +0200 |
wenzelm |
prefer warm start via JEdit_Main;
|
changeset |
files
|
| Fri, 06 Sep 2013 20:59:36 +0200 |
haftmann |
slight cleanup of lemma locations; tuned proof
|
changeset |
files
|
| Fri, 06 Sep 2013 20:55:14 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 06 Sep 2013 15:47:51 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Sep 2013 12:46:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Sep 2013 12:22:00 +0200 |
wenzelm |
removed junk;
|
changeset |
files
|
| Fri, 06 Sep 2013 12:05:01 +0200 |
wenzelm |
more standard header;
|
changeset |
files
|
| Fri, 06 Sep 2013 12:00:58 +0200 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Fri, 06 Sep 2013 10:57:27 +0200 |
noschinl |
merged
|
changeset |
files
|
| Fri, 06 Sep 2013 10:56:40 +0200 |
noschinl |
added examples for Simps_Case_Conv
|
changeset |
files
|
| Fri, 06 Sep 2013 10:56:40 +0200 |
noschinl |
allowed less exhaustive patterns
|
changeset |
files
|
| Fri, 06 Sep 2013 10:56:40 +0200 |
noschinl |
use case_of_simps
|
changeset |
files
|
| Fri, 06 Sep 2013 10:56:40 +0200 |
noschinl |
use case_of_simps
|
changeset |
files
|
| Fri, 06 Sep 2013 10:56:40 +0200 |
noschinl |
added simps_of_case and case_of_simps to convert between simps and case rules
|
changeset |
files
|
| Thu, 05 Sep 2013 23:14:28 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 05 Sep 2013 22:08:25 +0200 |
wenzelm |
close window and start process asynchronously;
|
changeset |
files
|
| Thu, 05 Sep 2013 21:37:32 +0200 |
wenzelm |
more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;
|
changeset |
files
|
| Thu, 05 Sep 2013 21:11:16 +0200 |
wenzelm |
recovered cygwin.root from 1c87e79bb838;
|
changeset |
files
|
| Thu, 05 Sep 2013 20:37:24 +0200 |
wenzelm |
provide file indicator;
|
changeset |
files
|
| Thu, 05 Sep 2013 20:26:41 +0200 |
wenzelm |
updated windows_app-20130905;
|
changeset |
files
|
| Thu, 05 Sep 2013 20:19:22 +0200 |
wenzelm |
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
|
changeset |
files
|
| Thu, 05 Sep 2013 16:39:01 +0200 |
wenzelm |
standardize jdk name;
|
changeset |
files
|
| Thu, 05 Sep 2013 16:03:44 +0200 |
wenzelm |
updated to jdk-7u25;
|
changeset |
files
|
| Thu, 05 Sep 2013 13:09:31 +0200 |
wenzelm |
support only one scala version;
|
changeset |
files
|
| Thu, 05 Sep 2013 12:33:51 +0200 |
wenzelm |
updated to jedit_build-20130905 which is based on jedit-5.1.0;
|
changeset |
files
|
| Thu, 05 Sep 2013 18:05:03 +0200 |
haftmann |
explicit module names have precedence over identifier declarations
|
changeset |
files
|
| Thu, 05 Sep 2013 18:05:02 +0200 |
haftmann |
check explicit module names for conformity
|
changeset |
files
|
| Thu, 05 Sep 2013 11:10:51 +0200 |
traytel |
list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
|
changeset |
files
|
| Thu, 05 Sep 2013 01:58:48 +0200 |
panny |
support indirect corecursion
|
changeset |
files
|
| Wed, 04 Sep 2013 23:57:38 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 04 Sep 2013 22:37:19 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 04 Sep 2013 21:25:03 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 04 Sep 2013 17:40:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 04 Sep 2013 17:36:37 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 04 Sep 2013 17:35:47 +0200 |
wenzelm |
interpret keys more movement only when needed;
|
changeset |
files
|
| Wed, 04 Sep 2013 16:03:45 +0200 |
wenzelm |
non-persistent print_state: trade-off between JVM space vs. ML time;
|
changeset |
files
|
| Wed, 04 Sep 2013 15:27:24 +0200 |
wenzelm |
some explicit indication of Proof General legacy;
|
changeset |
files
|
| Wed, 04 Sep 2013 13:45:46 +0200 |
panny |
merge
|
changeset |
files
|
| Wed, 04 Sep 2013 02:11:50 +0200 |
panny |
various refactoring;
|
changeset |
files
|
| Wed, 04 Sep 2013 13:22:03 +0200 |
wenzelm |
expose basic Symbol.properties (uninterpreted);
|
changeset |
files
|
| Wed, 04 Sep 2013 13:13:14 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 04 Sep 2013 12:20:00 +0200 |
wenzelm |
remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
|
changeset |
files
|
| Wed, 04 Sep 2013 11:12:00 +0200 |
wenzelm |
no completion on backspace -- too intrusive, e.g. when deleting keywords;
|
changeset |
files
|
| Wed, 04 Sep 2013 10:46:57 +0200 |
wenzelm |
more contributors;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:42 +0100 |
sultana |
updated TPTP parser to conform to version 5.5.0 (but excluding the TPI language since its parser spec is still incomplete);
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:41 +0100 |
sultana |
updated TPTP parser to conform to version 5.4.0;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:41 +0100 |
sultana |
included axiom formulas (removing a FIXME) in the imported problem;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:41 +0100 |
sultana |
updated syntax to use 'ML_file' rather than 'uses';
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:41 +0100 |
sultana |
now allowing numeric identifiers to be used in 'file' annotations;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:40 +0100 |
sultana |
get_file_list now returns files sorted by size;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:40 +0100 |
sultana |
brought up to date with TPTP_Proof;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:40 +0100 |
sultana |
using richer annotation from formula annotations in proof;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:40 +0100 |
sultana |
extracting more info from formula annotation in proof;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:40 +0100 |
sultana |
corrected syntax filter;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:40 +0100 |
sultana |
reading tptp status code;
|
changeset |
files
|
| Tue, 03 Sep 2013 21:46:40 +0100 |
sultana |
improved handling of nonstandard problem names;
|
changeset |
files
|
| Tue, 03 Sep 2013 22:30:52 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 03 Sep 2013 22:10:54 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 03 Sep 2013 22:04:23 +0200 |
wenzelm |
tuned proofs -- less guessing;
|
changeset |
files
|
| Tue, 03 Sep 2013 19:58:00 +0200 |
wenzelm |
cases: formal binding of 'assumes', with position provided via invoke_case;
|
changeset |
files
|
| Tue, 03 Sep 2013 18:21:43 +0200 |
wenzelm |
minor tuning;
|
changeset |
files
|
| Tue, 03 Sep 2013 13:09:15 +0200 |
wenzelm |
cases: more position information and PIDE markup;
|
changeset |
files
|
| Tue, 03 Sep 2013 11:58:34 +0200 |
wenzelm |
more liberal 'case' syntax: allow parentheses without arguments;
|
changeset |
files
|
| Tue, 03 Sep 2013 11:55:59 +0200 |
wenzelm |
more robust ToyList_Test;
|
changeset |
files
|
| Tue, 03 Sep 2013 11:29:01 +0200 |
wenzelm |
Execution.fork formally requires registered Execution.running;
|
changeset |
files
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
changeset |
files
|
| Tue, 03 Sep 2013 00:51:08 +0200 |
wenzelm |
proper imports;
|
changeset |
files
|
| Mon, 02 Sep 2013 23:35:58 +0200 |
wenzelm |
tuned proof;
|
changeset |
files
|
| Mon, 02 Sep 2013 16:10:26 +0200 |
wenzelm |
more explicit indication of 'guess' as improper Isar (aka "script") element;
|
changeset |
files
|
| Tue, 03 Sep 2013 22:12:48 +0200 |
ballarin |
Further clarifies sublocale and rewrite morphisms.
|
changeset |
files
|
| Tue, 03 Sep 2013 22:12:48 +0200 |
ballarin |
Clarifies that interpretation does not only apply to facts, but to declaratoins in general.
|
changeset |
files
|
| Tue, 03 Sep 2013 22:12:48 +0200 |
ballarin |
Clarifies documentation of interpretation in local theories.
|
changeset |
files
|
| Tue, 03 Sep 2013 22:12:47 +0200 |
ballarin |
New test case: interpretation in named contexts is not persistent.
|
changeset |
files
|
| Tue, 03 Sep 2013 22:12:47 +0200 |
ballarin |
Terminology: mixin -> rewrite morphism.
|
changeset |
files
|
| Mon, 02 Sep 2013 17:57:56 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 02 Sep 2013 17:12:59 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Mon, 02 Sep 2013 17:14:51 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Mon, 02 Sep 2013 17:14:35 +0200 |
Andreas Lochbihler |
NEWS
|
changeset |
files
|
| Mon, 02 Sep 2013 16:28:11 +0200 |
Andreas Lochbihler |
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
|
changeset |
files
|
| Mon, 02 Sep 2013 15:13:00 +0200 |
panny |
handle direct corecursion
|
changeset |
files
|
| Mon, 02 Sep 2013 11:03:02 +0200 |
wenzelm |
updated according to bceec99254b0;
|
changeset |
files
|
| Sun, 01 Sep 2013 14:00:05 +0200 |
panny |
improved interfaces
|
changeset |
files
|
| Sun, 01 Sep 2013 10:45:54 +0200 |
panny |
simplified rewriting of map arguments
|
changeset |
files
|
| Sun, 01 Sep 2013 16:38:04 +1000 |
kleing |
remove redundant (simp del: ..)
|
changeset |
files
|
| Sun, 01 Sep 2013 00:37:53 +0200 |
traytel |
modernized more examples
|
changeset |
files
|
| Sat, 31 Aug 2013 23:55:03 +0200 |
traytel |
merged
|
changeset |
files
|
| Sat, 31 Aug 2013 23:49:36 +0200 |
traytel |
modernized example
|
changeset |
files
|
| Sat, 31 Aug 2013 23:49:14 +0200 |
traytel |
honor mixfix specifications
|
changeset |
files
|
| Sat, 31 Aug 2013 23:52:32 +0200 |
panny |
merge
|
changeset |
files
|
| Sat, 31 Aug 2013 20:37:31 +0200 |
panny |
simplified recursive calls' replacement
|
changeset |
files
|
| Sat, 31 Aug 2013 22:32:43 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 31 Aug 2013 22:18:51 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sat, 31 Aug 2013 18:12:51 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sat, 31 Aug 2013 13:34:39 +0200 |
wenzelm |
provide ISABELLE_JAVA_SYSTEM_OPTIONS via settings;
|
changeset |
files
|
| Sat, 31 Aug 2013 13:20:18 +0200 |
wenzelm |
uniform abbrevs for left/right arrows;
|
changeset |
files
|
| Sat, 31 Aug 2013 13:05:04 +0200 |
wenzelm |
more abbrevs according to Isabelle/HOL ASCII replacement syntax;
|
changeset |
files
|
| Sat, 31 Aug 2013 12:53:39 +0200 |
wenzelm |
added common alternative for == (its ambiguity also avoids conflict with ==>);
|
changeset |
files
|
| Sat, 31 Aug 2013 12:14:19 +0200 |
wenzelm |
more accurate description: Swing/L&F has additional handlers;
|
changeset |
files
|
| Sat, 31 Aug 2013 18:18:33 +0200 |
panny |
handle selector formulae with no corecursive calls
|
changeset |
files
|
| Sat, 31 Aug 2013 00:40:21 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 31 Aug 2013 00:39:59 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 30 Aug 2013 23:41:09 +0200 |
wenzelm |
simplified (see 7c39677f9ea0);
|
changeset |
files
|
| Fri, 30 Aug 2013 23:38:18 +0200 |
wenzelm |
sort items according to persistent history of frequency of use;
|
changeset |
files
|
| Fri, 30 Aug 2013 22:22:07 +0200 |
wenzelm |
more general backup files;
|
changeset |
files
|
| Fri, 30 Aug 2013 21:43:15 +0200 |
panny |
fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)
|
changeset |
files
|
| Fri, 30 Aug 2013 21:14:38 +0200 |
wenzelm |
some tests on /home/polyml/polyml-svn, which is approaching polyml-5.5.1;
|
changeset |
files
|
| Fri, 30 Aug 2013 18:22:17 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 30 Aug 2013 15:54:23 +0200 |
traytel |
Doc improvements
|
changeset |
files
|
| Fri, 30 Aug 2013 15:36:00 +0200 |
traytel |
prove theorem in the right context (that knows about local variables)
|
changeset |
files
|
| Fri, 30 Aug 2013 15:05:04 +0200 |
blanchet |
fixed docs w.r.t. availability of "primrec_new" and friends
|
changeset |
files
|
| Fri, 30 Aug 2013 14:17:19 +0200 |
blanchet |
more canonical naming
|
changeset |
files
|
| Fri, 30 Aug 2013 14:07:49 +0200 |
nipkow |
more set syntax
|
changeset |
files
|
| Fri, 30 Aug 2013 13:46:32 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 30 Aug 2013 13:45:57 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Fri, 30 Aug 2013 13:24:14 +0200 |
wenzelm |
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
|
changeset |
files
|
| Fri, 30 Aug 2013 12:59:28 +0200 |
wenzelm |
explicit is always immediate;
|
changeset |
files
|
| Fri, 30 Aug 2013 12:46:32 +0200 |
wenzelm |
single-letter abbrev does not make sense -- too many candidates;
|
changeset |
files
|
| Fri, 30 Aug 2013 12:44:39 +0200 |
wenzelm |
allow short words for explicit completion;
|
changeset |
files
|
| Fri, 30 Aug 2013 12:33:16 +0200 |
wenzelm |
fewer conflicts -- adhoc resolution of == vs. ==> via unicode (!) image;
|
changeset |
files
|
| Fri, 30 Aug 2013 12:24:15 +0200 |
wenzelm |
more symbol abbrevs;
|
changeset |
files
|
| Fri, 30 Aug 2013 12:10:34 +0200 |
wenzelm |
misc tuning -- reduce conflicts;
|
changeset |
files
|
| Fri, 30 Aug 2013 12:09:53 +0200 |
wenzelm |
allow multiple entries;
|
changeset |
files
|
| Fri, 30 Aug 2013 11:41:43 +0200 |
wenzelm |
more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
|
changeset |
files
|
| Fri, 30 Aug 2013 11:04:29 +0200 |
wenzelm |
allow multiple symbol properties, notably groups and abbrevs;
|
changeset |
files
|
| Fri, 30 Aug 2013 11:00:46 +0200 |
wenzelm |
private copy (!) of etc/symbols for WWW_Find, which has its own interpretation of the file format;
|
changeset |
files
|
| Fri, 30 Aug 2013 10:07:20 +0200 |
wenzelm |
check tar error, e.g. from corrupted download;
|
changeset |
files
|
| Fri, 30 Aug 2013 10:01:25 +0200 |
wenzelm |
less surprising immediate completion;
|
changeset |
files
|
| Fri, 30 Aug 2013 13:23:23 +0200 |
blanchet |
updated keywords
|
changeset |
files
|
| Fri, 30 Aug 2013 12:43:39 +0200 |
blanchet |
tuned theory name
|
changeset |
files
|
| Fri, 30 Aug 2013 12:37:03 +0200 |
blanchet |
moved keywords down the hierarchy
|
changeset |
files
|
| Fri, 30 Aug 2013 12:12:41 +0200 |
blanchet |
renamed command to clarify connection with BNF
|
changeset |
files
|
| Fri, 30 Aug 2013 12:09:51 +0200 |
blanchet |
merged two theory files
|
changeset |
files
|
| Fri, 30 Aug 2013 12:06:37 +0200 |
blanchet |
updated news/contributors with BNF stuff
|
changeset |
files
|
| Fri, 30 Aug 2013 12:06:11 +0200 |
blanchet |
added example
|
changeset |
files
|
| Fri, 30 Aug 2013 12:05:22 +0200 |
blanchet |
rationalized files
|
changeset |
files
|
| Fri, 30 Aug 2013 11:37:22 +0200 |
blanchet |
polished newly included files after moving
|
changeset |
files
|
| Fri, 30 Aug 2013 11:27:23 +0200 |
blanchet |
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
|
changeset |
files
|
| Fri, 30 Aug 2013 00:11:01 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 29 Aug 2013 23:22:58 +0200 |
traytel |
merged
|
changeset |
files
|
| Thu, 29 Aug 2013 23:21:48 +0200 |
traytel |
qualify internal and external constants in {l,g}fp properly
|
changeset |
files
|
| Thu, 29 Aug 2013 23:13:17 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 29 Aug 2013 22:53:17 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 29 Aug 2013 22:40:50 +0200 |
wenzelm |
border as for Pretty_Tooltip;
|
changeset |
files
|
| Thu, 29 Aug 2013 22:35:50 +0200 |
wenzelm |
less aggressive immediate completion, based on input and text;
|
changeset |
files
|
| Thu, 29 Aug 2013 22:08:02 +0200 |
wenzelm |
preserve original word -- relevant for true uniqueness of immediate completion;
|
changeset |
files
|
| Thu, 29 Aug 2013 21:53:29 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 29 Aug 2013 21:49:46 +0200 |
wenzelm |
added action isabelle.complete, using standard jEdit keyboard shortcut;
|
changeset |
files
|
| Thu, 29 Aug 2013 21:17:46 +0200 |
wenzelm |
option to insert unique completion immediately into buffer;
|
changeset |
files
|
| Thu, 29 Aug 2013 20:46:55 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 29 Aug 2013 23:01:04 +0200 |
blanchet |
renamed BNF fact
|
changeset |
files
|
| Thu, 29 Aug 2013 22:56:39 +0200 |
blanchet |
renamed BNF axiom
|
changeset |
files
|
| Thu, 29 Aug 2013 22:39:46 +0200 |
blanchet |
renamed BNF fact
|
changeset |
files
|