| Thu, 10 Apr 2014 17:48:14 +0200 |
kuncar |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
changeset |
files
|
| Thu, 10 Apr 2014 17:48:13 +0200 |
kuncar |
tuned
|
changeset |
files
|
| Thu, 10 Apr 2014 15:14:38 +0200 |
traytel |
more accurate type arguments for intermeadiate typedefs
|
changeset |
files
|
| Thu, 10 Apr 2014 14:40:11 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 10 Apr 2014 14:36:29 +0200 |
wenzelm |
ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL;
|
changeset |
files
|
| Thu, 10 Apr 2014 14:27:35 +0200 |
wenzelm |
more standard names;
|
changeset |
files
|
| Thu, 10 Apr 2014 12:48:01 +0200 |
wenzelm |
modernized simproc_setup;
|
changeset |
files
|
| Thu, 10 Apr 2014 12:30:02 +0200 |
wenzelm |
modernized theory setup;
|
changeset |
files
|
| Thu, 10 Apr 2014 12:22:29 +0200 |
wenzelm |
added simproc markup, which also indicates legacy simprocs outside the name space;
|
changeset |
files
|
| Thu, 10 Apr 2014 12:00:25 +0200 |
wenzelm |
modernized simproc_setup;
|
changeset |
files
|
| Thu, 10 Apr 2014 11:24:58 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Thu, 10 Apr 2014 11:06:45 +0200 |
wenzelm |
more contributors;
|
changeset |
files
|
| Thu, 10 Apr 2014 10:36:29 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 10 Apr 2014 10:30:32 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Thu, 10 Apr 2014 10:27:29 +0200 |
wenzelm |
tuned error -- allow user to click on hyperlink to open remote file;
|
changeset |
files
|
| Thu, 10 Apr 2014 10:06:54 +0200 |
wenzelm |
no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;
|
changeset |
files
|
| Wed, 09 Apr 2014 23:22:58 +0200 |
wenzelm |
improved support for external URLs, based on standard Java network operations;
|
changeset |
files
|
| Wed, 09 Apr 2014 23:04:20 +0200 |
wenzelm |
basic URL operations (with Isabelle/Scala error handling);
|
changeset |
files
|
| Wed, 09 Apr 2014 20:58:32 +0200 |
wenzelm |
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
|
changeset |
files
|
| Wed, 09 Apr 2014 17:54:09 +0200 |
wenzelm |
allow text cartouches in regular outer syntax categories "text" and "altstring";
|
changeset |
files
|
| Wed, 09 Apr 2014 17:29:37 +0200 |
wenzelm |
tuned comments (see Scala version);
|
changeset |
files
|
| Wed, 09 Apr 2014 16:22:06 +0200 |
wenzelm |
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
|
changeset |
files
|
| Wed, 09 Apr 2014 15:19:22 +0200 |
wenzelm |
clarifed results range;
|
changeset |
files
|
| Wed, 09 Apr 2014 15:03:07 +0200 |
wenzelm |
more explicit message discrimination;
|
changeset |
files
|
| Wed, 09 Apr 2014 13:32:34 +0200 |
wenzelm |
avoid confusion about pointless cursor movement with external links;
|
changeset |
files
|
| Wed, 09 Apr 2014 12:33:02 +0200 |
wenzelm |
prefer regular Goal_Display.pretty_goals, without censorship of options;
|
changeset |
files
|
| Wed, 09 Apr 2014 12:28:24 +0200 |
wenzelm |
more standard names;
|
changeset |
files
|
| Wed, 09 Apr 2014 12:22:57 +0200 |
wenzelm |
proper context for print_tac;
|
changeset |
files
|
| Wed, 09 Apr 2014 11:32:41 +0200 |
wenzelm |
more conventional tactic programming;
|
changeset |
files
|
| Wed, 09 Apr 2014 10:44:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 10 Apr 2014 11:34:55 +0200 |
traytel |
reintroduce example (cf. 39281b3e4fac)
|
changeset |
files
|
| Thu, 10 Apr 2014 10:52:48 +0200 |
traytel |
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
|
changeset |
files
|
| Thu, 10 Apr 2014 09:38:38 +0200 |
traytel |
made N2M tactic more robust
|
changeset |
files
|
| Wed, 09 Apr 2014 18:40:21 +0200 |
blanchet |
generate cliques for 'prim(co)rec' N2M
|
changeset |
files
|
| Wed, 09 Apr 2014 18:22:11 +0200 |
blanchet |
thread mutual cliques through
|
changeset |
files
|
| Wed, 09 Apr 2014 13:15:21 +0200 |
hoelzl |
generalize ln/log_powr; add log_base_powr/pow
|
changeset |
files
|
| Wed, 09 Apr 2014 10:04:31 +0200 |
haftmann |
parametricity transfer rule for INFIMUM, SUPREMUM
|
changeset |
files
|
| Wed, 09 Apr 2014 09:37:49 +0200 |
hoelzl |
add divide_simps
|
changeset |
files
|
| Wed, 09 Apr 2014 09:37:48 +0200 |
hoelzl |
field_simps: better support for negation and division, and power
|
changeset |
files
|
| Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
changeset |
files
|
| Tue, 08 Apr 2014 23:16:00 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 08 Apr 2014 23:05:21 +0200 |
wenzelm |
more native rm_tree, using Java 7 facilities;
|
changeset |
files
|
| Tue, 08 Apr 2014 22:24:00 +0200 |
wenzelm |
expose more bad cases;
|
changeset |
files
|
| Tue, 08 Apr 2014 22:01:08 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 08 Apr 2014 21:48:09 +0200 |
wenzelm |
more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
|
changeset |
files
|
| Tue, 08 Apr 2014 20:03:00 +0200 |
wenzelm |
simplified Text.Chunk -- eliminated ooddities;
|
changeset |
files
|
| Tue, 08 Apr 2014 20:00:53 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 08 Apr 2014 19:35:50 +0200 |
wenzelm |
more frugal Symbol.Index -- no need to waste space on mostly empty arrays;
|
changeset |
files
|
| Tue, 08 Apr 2014 19:17:28 +0200 |
wenzelm |
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
|
changeset |
files
|
| Tue, 08 Apr 2014 16:07:02 +0200 |
wenzelm |
avoid data redundancy;
|
changeset |
files
|
| Tue, 08 Apr 2014 15:12:54 +0200 |
wenzelm |
tuned signature -- moved Command.Chunk to Text.Chunk;
|
changeset |
files
|
| Tue, 08 Apr 2014 14:59:36 +0200 |
wenzelm |
more uniform ML/document antiquotations;
|
changeset |
files
|
| Tue, 08 Apr 2014 14:56:55 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Tue, 08 Apr 2014 14:15:48 +0200 |
wenzelm |
more positions and markup;
|
changeset |
files
|
| Tue, 08 Apr 2014 13:24:08 +0200 |
wenzelm |
more precise token positions;
|
changeset |
files
|
| Tue, 08 Apr 2014 12:31:17 +0200 |
wenzelm |
more uniform Command.Chunk operations;
|
changeset |
files
|
| Tue, 08 Apr 2014 12:19:33 +0200 |
wenzelm |
more explicit Command.Chunk types, less ooddities;
|
changeset |
files
|
| Tue, 08 Apr 2014 10:24:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 08 Apr 2014 09:48:38 +0200 |
wenzelm |
ignore deps_changed (again) -- avoid proactive load attempts of unfinished header specification while the user is typing;
|
changeset |
files
|
| Tue, 08 Apr 2014 09:45:13 +0200 |
wenzelm |
no report for position singularity, notably for aux. file, especially empty one;
|
changeset |
files
|
| Mon, 07 Apr 2014 23:02:29 +0200 |
wenzelm |
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
|
changeset |
files
|
| Mon, 07 Apr 2014 21:23:02 +0200 |
wenzelm |
tuned signature -- prefer static type Document.Node.Name;
|
changeset |
files
|
| Tue, 08 Apr 2014 18:48:10 +0200 |
blanchet |
commented out example that triggers a bug
|
changeset |
files
|
| Tue, 08 Apr 2014 18:16:47 +0200 |
blanchet |
allow arguments to 'datatype_compat' in disorder
|
changeset |
files
|
| Tue, 08 Apr 2014 18:06:21 +0200 |
blanchet |
added 'datatype_compat' examples/tests
|
changeset |
files
|
| Tue, 08 Apr 2014 17:49:03 +0200 |
blanchet |
support deeply nested datatypes in 'datatype_compat'
|
changeset |
files
|
| Tue, 08 Apr 2014 13:47:27 +0200 |
blanchet |
preserve user type variable names to avoid mismatches/confusion
|
changeset |
files
|
| Tue, 08 Apr 2014 12:46:38 +0200 |
haftmann |
even more standardized doc session names after #b266e7a86485
|
changeset |
files
|
| Mon, 07 Apr 2014 16:37:57 +0200 |
wenzelm |
refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
|
changeset |
files
|
| Mon, 07 Apr 2014 13:55:12 +0200 |
wenzelm |
support for URL as file name, similar to treatment in jEdit.java;
|
changeset |
files
|
| Mon, 07 Apr 2014 13:11:31 +0200 |
wenzelm |
provide old-style ISABELLE_SCALA_SCRIPT for uniformity;
|
changeset |
files
|
| Mon, 07 Apr 2014 13:06:34 +0200 |
wenzelm |
separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
|
changeset |
files
|
| Sun, 06 Apr 2014 21:01:45 +0200 |
nipkow |
merged
|
changeset |
files
|
| Sun, 06 Apr 2014 21:01:33 +0200 |
nipkow |
tuned lemmas: more general class
|
changeset |
files
|
| Sun, 06 Apr 2014 19:35:35 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 06 Apr 2014 19:16:34 +0200 |
wenzelm |
removed abbrev "<-" again (see c771f0fe28d1) due to conflict with important "<->" and "<-->";
|
changeset |
files
|
| Sun, 06 Apr 2014 17:19:08 +0200 |
nipkow |
merged
|
changeset |
files
|
| Sun, 06 Apr 2014 17:18:57 +0200 |
nipkow |
made field_simps "more complete"
|
changeset |
files
|
| Sun, 06 Apr 2014 17:09:32 +0200 |
wenzelm |
shell functions for all Isabelle executables;
|
changeset |
files
|
| Sun, 06 Apr 2014 16:59:41 +0200 |
wenzelm |
renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
|
changeset |
files
|
| Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
changeset |
files
|
| Sun, 06 Apr 2014 15:51:02 +0200 |
wenzelm |
clarified position: no offset here;
|
changeset |
files
|
| Sun, 06 Apr 2014 15:43:45 +0200 |
wenzelm |
more source positions;
|
changeset |
files
|
| Sun, 06 Apr 2014 15:38:54 +0200 |
wenzelm |
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
|
changeset |
files
|
| Sun, 06 Apr 2014 15:19:22 +0200 |
wenzelm |
clarified ML bootstrap;
|
changeset |
files
|
| Sun, 06 Apr 2014 14:30:26 +0200 |
wenzelm |
prepare "back" position for Navigator, before following hyperlink;
|
changeset |
files
|
| Sat, 05 Apr 2014 23:56:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 05 Apr 2014 23:42:30 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 05 Apr 2014 23:36:00 +0200 |
wenzelm |
more uniform build options;
|
changeset |
files
|
| Sat, 05 Apr 2014 23:17:30 +0200 |
wenzelm |
re-implemented build_doc in Isabelle/Scala;
|
changeset |
files
|
| Sat, 05 Apr 2014 22:37:17 +0200 |
wenzelm |
more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
|
changeset |
files
|
| Sat, 05 Apr 2014 20:08:00 +0200 |
wenzelm |
more standard hash-bang (python *is* canonical according to Admin/PLATFORMS);
|
changeset |
files
|
| Sat, 05 Apr 2014 19:16:44 +0200 |
wenzelm |
tuned -- just one qualification of sections ("!");
|
changeset |
files
|
| Sat, 05 Apr 2014 19:16:16 +0200 |
wenzelm |
tuned error;
|
changeset |
files
|
| Sat, 05 Apr 2014 19:07:05 +0200 |
wenzelm |
proper settings instead of hard-wired information;
|
changeset |
files
|
| Sat, 05 Apr 2014 18:52:03 +0200 |
wenzelm |
explicit indication of important doc sections ("!"), which are expanded in the tree view;
|
changeset |
files
|
| Sat, 05 Apr 2014 18:14:54 +0200 |
wenzelm |
clarified Doc entry: more explicit path;
|
changeset |
files
|
| Sat, 05 Apr 2014 15:03:40 +0200 |
wenzelm |
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
|
changeset |
files
|
| Sat, 05 Apr 2014 11:37:00 +0200 |
haftmann |
closer correspondence of document and session names, while maintaining document names for external reference
|
changeset |
files
|
| Sat, 05 Apr 2014 17:52:29 +0100 |
paulson |
ignore jedit mark files
|
changeset |
files
|
| Sat, 05 Apr 2014 10:12:51 +0200 |
haftmann |
avoid romanism
|
changeset |
files
|
| Sat, 05 Apr 2014 10:03:04 +0200 |
haftmann |
churning pie charts (with non-canonical prerequisites!)
|
changeset |
files
|
| Sat, 05 Apr 2014 10:03:03 +0200 |
haftmann |
CONTRIBUTORS
|
changeset |
files
|
| Sat, 05 Apr 2014 10:01:07 +0200 |
haftmann |
proper inclusion into library
|
changeset |
files
|
| Sat, 05 Apr 2014 01:04:46 +0100 |
paulson |
A single [simp] to handle the case -a/-b.
|
changeset |
files
|
| Fri, 04 Apr 2014 22:51:22 +0200 |
wenzelm |
support for jEdit Navigator plugin;
|
changeset |
files
|
| Fri, 04 Apr 2014 22:21:46 +0200 |
wenzelm |
more permissive Session.update_options: this is wired to jEdit PropertiesChanged, which may occur before the prover is started;
|
changeset |
files
|
| Fri, 04 Apr 2014 19:09:56 +0200 |
blanchet |
added option to Mirabelle
|
changeset |
files
|
| Fri, 04 Apr 2014 17:58:25 +0100 |
paulson |
divide_minus_left divide_minus_right are in field_simps but are not default simprules
|
changeset |
files
|
| Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
changeset |
files
|
| Fri, 04 Apr 2014 16:43:47 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Fri, 04 Apr 2014 15:58:20 +0200 |
wenzelm |
tuned rendering -- take 1px line border into account;
|
changeset |
files
|
| Fri, 04 Apr 2014 14:31:31 +0200 |
wenzelm |
revert ce37fcb30cf2 for the sake of Mac OS X -- let some event listeners of jEdit reset the cursor;
|
changeset |
files
|
| Fri, 04 Apr 2014 13:12:16 +0200 |
wenzelm |
tuned white space;
|
changeset |
files
|
| Fri, 04 Apr 2014 15:56:40 +0200 |
blanchet |
use Z3 TPTP cores rather than proofs since the latter are somewhat broken
|
changeset |
files
|
| Fri, 04 Apr 2014 14:44:51 +0200 |
blanchet |
tuned spaces
|
changeset |
files
|
| Fri, 04 Apr 2014 13:22:26 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Fri, 04 Apr 2014 13:22:15 +0200 |
Andreas Lochbihler |
add missing adaptation for narrowing to work with variables of type integer => integer
|
changeset |
files
|
| Fri, 04 Apr 2014 12:37:57 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 04 Apr 2014 12:07:48 +0200 |
wenzelm |
added ML antiquotation @{print};
|
changeset |
files
|