| Sat, 19 Sep 2015 21:09:38 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 15 Sep 2015 11:18:25 +0200 |
lammich |
Omega_Words_Fun: Infinite words as functions from nat.
|
file |
diff |
annotate
|
| Mon, 14 Sep 2015 17:39:29 +0200 |
wenzelm |
replacement character for spaces;
|
file |
diff |
annotate
|
| Mon, 14 Sep 2015 16:44:09 +0200 |
wenzelm |
single-instance application, even on Linux;
|
file |
diff |
annotate
|
| Mon, 14 Sep 2015 16:06:32 +0200 |
wenzelm |
added isabelle jedit_client;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 20:20:16 +0200 |
wenzelm |
renamed method "goals" to "goal_cases" to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 11 Sep 2015 17:57:34 +0200 |
wenzelm |
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
|
file |
diff |
annotate
|
| Thu, 10 Sep 2015 11:59:12 +0200 |
haftmann |
dropped redundant NEWS
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 14:47:41 +0200 |
wenzelm |
eliminated \<Colon> from syntax of constraints;
|
file |
diff |
annotate
|
| Tue, 08 Sep 2015 17:34:46 +0200 |
wenzelm |
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
|
file |
diff |
annotate
|
| Tue, 08 Sep 2015 15:37:13 +0200 |
wenzelm |
clarified Java runtime options for 32 vs. 64 bit;
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
obsolete: if case_prod is fully applied, it is printed as proper case expression;
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 21:55:13 +0200 |
wenzelm |
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 14:51:49 +0200 |
wenzelm |
removed obsolete theory Legacy_Mrec;
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 13:37:18 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 22:45:40 +0200 |
wenzelm |
support x86_64-windows;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 21:01:21 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 16:48:05 +0200 |
blanchet |
eliminated obsolete environment variable
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 20:16:07 +0200 |
blanchet |
robust handling of Vampire 4 proofs
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 20:10:40 +0200 |
blanchet |
reverted 6ac3172985d4 -- the old URL has been restored
|
file |
diff |
annotate
|
| Fri, 21 Aug 2015 16:47:57 +0200 |
wenzelm |
updated to jdk-8u60, with support for x86_64-windows;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 17:39:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 14:31:09 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 14:13:00 +0200 |
wenzelm |
updated to polyml-5.5.3-20150820, with native x86-windows support;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:14:16 +0200 |
traytel |
tuned NEWS
|
file |
diff |
annotate
|
| Wed, 12 Aug 2015 20:46:33 +0200 |
traytel |
NEWS, CONTRIBUTORS, documentation for lift_bnf
|
file |
diff |
annotate
|
| Sat, 08 Aug 2015 10:51:33 +0200 |
haftmann |
direct bootstrap of integer division from natural division
|
file |
diff |
annotate
|
| Tue, 04 Aug 2015 23:11:16 +0200 |
wenzelm |
eliminated clone;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 16:16:13 +0100 |
paulson |
the Cauchy integral theorem and related material
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:56:08 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 22:26:11 +0200 |
wenzelm |
eliminated atac, rtac, etac, dtac, ftac;
|
file |
diff |
annotate
|
| Sun, 12 Jul 2015 13:04:42 +0200 |
Lars Hupel |
Quickcheck setup for finite sets
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 22:36:31 +0200 |
wenzelm |
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 14:01:41 +0200 |
haftmann |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Thu, 02 Jul 2015 14:09:43 +0200 |
wenzelm |
documentation for 'subgoal' command;
|
file |
diff |
annotate
|
| Wed, 01 Jul 2015 10:53:14 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2015 15:20:56 +0200 |
wenzelm |
renamed "default" to "standard", to make semantically clear what it is;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2015 10:40:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 20:55:46 +0200 |
wenzelm |
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
|
file |
diff |
annotate
|
| Sat, 27 Jun 2015 00:10:24 +0200 |
wenzelm |
premises in 'show' are treated like 'assume';
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 11:08:33 +0200 |
blanchet |
updated SystemOnTPTP URL
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 23:49:05 +0200 |
wenzelm |
implicit goal cases are legacy;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 21:45:00 +0200 |
wenzelm |
added method "goals" for proper subgoal cases;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2015 21:26:03 +0200 |
wenzelm |
clarified 'case' command;
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 20:36:33 +0200 |
wenzelm |
support 'when' statement, which corresponds to 'presume';
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 19:22:48 +0200 |
wenzelm |
added method "sleep";
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 16:48:27 +0200 |
wenzelm |
clarified nesting of Isar goal structure;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 21:33:03 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 20:14:50 +0200 |
wenzelm |
discontinued unused 'defer_recdef';
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 07:53:35 +0200 |
haftmann |
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 07:53:33 +0200 |
haftmann |
generalized some theorems about integral domains and moved to HOL theories
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 15:55:22 +0200 |
nipkow |
renamed multiset_of -> mset
|
file |
diff |
annotate
|
| Thu, 18 Jun 2015 16:17:51 +0200 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 17:33:22 +0200 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| Mon, 15 Jun 2015 16:59:27 +0200 |
wenzelm |
vacuous fact `TERM x`;
|
file |
diff |
annotate
|
| Mon, 15 Jun 2015 00:23:18 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 23:22:08 +0200 |
wenzelm |
improved treatment of Element.Obtains via Expression.prepare_stmt;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 22:44:22 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 22:42:23 +0200 |
wenzelm |
more on 'consider' and related concepts;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 17:14:05 +0200 |
wenzelm |
implicit rule for method "cases";
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 13:09:05 +0200 |
wenzelm |
renamed "prems" to "that";
|
file |
diff |
annotate
|
| Fri, 12 Jun 2015 08:53:23 +0200 |
haftmann |
uniform _ div _ as infix syntax for ring division
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 18:57:31 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 14:46:31 +0200 |
wenzelm |
support for "if prems" in local goal statements;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 22:24:33 +0200 |
wenzelm |
more uniform treatment of auto bindings vs. explicit user bindings;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 16:07:11 +0200 |
wenzelm |
allow for_fixes for 'have', 'show' etc.;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 13:42:58 +0200 |
wenzelm |
clarified abstracted term bindings (again, see c8384ff11711);
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 15:50:17 +0200 |
fleury |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 13:38:19 +0200 |
Mathias Fleury |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 13:24:16 +0200 |
Mathias Fleury |
Renaming multiset operators < ~> <#,...
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 21:23:28 +0200 |
wenzelm |
clarified abstracted term bindings;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 19:38:08 +0200 |
wenzelm |
more careful treatment of term bindings in 'obtain' proof body;
|
file |
diff |
annotate
|
| Fri, 05 Jun 2015 13:41:06 +0200 |
wenzelm |
added Isar command 'supply';
|
file |
diff |
annotate
|
| Fri, 05 Jun 2015 13:26:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
explicit argument expansion of uncheck rules;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 15:06:09 +0200 |
wenzelm |
discontinued legacy;
|
file |
diff |
annotate
|
| Fri, 29 May 2015 17:56:43 +0200 |
blanchet |
removed model checks from Nitpick
|
file |
diff |
annotate
|
| Thu, 28 May 2015 10:18:46 +0200 |
blanchet |
made Auto Sledgehammer behave more like the real thing
|
file |
diff |
annotate
|
| Mon, 25 May 2015 22:11:43 +0200 |
wenzelm |
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
|
file |
diff |
annotate
|
| Sat, 23 May 2015 17:19:37 +0200 |
wenzelm |
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
Isabelle2015
|
file |
diff |
annotate
|
| Sun, 17 May 2015 23:03:49 +0200 |
wenzelm |
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
|
file |
diff |
annotate
|
| Thu, 07 May 2015 22:12:05 +0200 |
wenzelm |
use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;
|
file |
diff |
annotate
|
| Tue, 05 May 2015 16:52:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 04 May 2015 22:11:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 04 May 2015 14:16:20 +0200 |
kuncar |
NEWS
|
file |
diff |
annotate
|
| Mon, 04 May 2015 16:01:36 +0200 |
nipkow |
no more simp_legacy_precond
|
file |
diff |
annotate
|
| Sun, 19 Apr 2015 21:26:50 +0200 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 17:49:19 +0200 |
wenzelm |
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 15:54:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 14:57:25 +0200 |
wenzelm |
tuned for release;
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 13:01:09 +0200 |
traytel |
(low importance) NEWS
|
file |
diff |
annotate
|
| Fri, 17 Apr 2015 11:28:57 +0200 |
wenzelm |
allow to exclude session groups;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 14:18:32 +0200 |
wenzelm |
explicit error for Toplevel.proof_of;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 13:48:10 +0200 |
wenzelm |
clarified thy_deps;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 11:22:36 +0200 |
wenzelm |
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
|
file |
diff |
annotate
|
| Wed, 15 Apr 2015 21:20:37 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 14 Apr 2015 22:54:07 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 00:26:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 22:18:33 +0100 |
paulson |
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 12:47:46 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 12:40:03 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 23:56:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 12:16:45 +0200 |
nipkow |
renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:38 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 18:00:58 +0200 |
blanchet |
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:24:32 +0200 |
blanchet |
tuned wording
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:15:55 +0200 |
blanchet |
Z3 news
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 15:21:20 +0200 |
blanchet |
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 11:13:53 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 18:21:56 +0200 |
nipkow |
Removed mcard because it is equal to size
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 22:01:30 +0200 |
wenzelm |
some explanation of 'private';
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 22:40:41 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 22:08:06 +0200 |
wenzelm |
added command 'experiment';
|
file |
diff |
annotate
|