| Sun, 23 Feb 2014 10:44:57 +0100 |
haftmann |
NEWS and documentation, including correction of long-overseen "*"
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 10:33:43 +0100 |
haftmann |
dropped long-unused option
|
file |
diff |
annotate
|
| Sat, 22 Feb 2014 16:16:21 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 17:00:45 +0100 |
wenzelm |
improved completion based on context information;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:18:40 +0100 |
blanchet |
NEWS
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 16:56:51 +0100 |
wenzelm |
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 16:33:11 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 11:11:07 +0100 |
traytel |
reflect 207538943038 in NEWS
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 22:39:20 +0100 |
wenzelm |
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 14:07:26 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:33:28 +0100 |
blanchet |
folded 'rel_option' into 'option_rel'
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:33:28 +0100 |
blanchet |
folded 'list_all2' with the relator generated by 'datatype_new'
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 18:39:41 +0100 |
blanchet |
more NEWS
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 10:20:31 +0100 |
blanchet |
[mq]: news
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 22:08:18 +0100 |
wenzelm |
discontinued axiomatic 'classes', 'classrel', 'arities';
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 09:04:59 +0000 |
Lars Hupel |
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 01:35:48 +0100 |
blanchet |
removed legacy 'metisFT' method
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 17:18:38 +0100 |
blanchet |
added new option to documentation
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 14:37:53 +0100 |
blanchet |
renamed Sledgehammer options for symmetry between positive and negative versions
|
file |
diff |
annotate
|
| Sun, 26 Jan 2014 14:01:19 +0100 |
wenzelm |
discontinued obsolete attribute "standard";
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 22:06:07 +0100 |
wenzelm |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 16:59:41 +0100 |
wenzelm |
NEWS for 31afce809794;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 23:51:26 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 17:14:27 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 15:10:33 +0100 |
wenzelm |
inner syntax token language allows regular quoted strings;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2014 13:51:10 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Sun, 19 Jan 2014 22:38:17 +0100 |
boehmes |
removed obsolete remote_cvc3 and remote_z3
|
file |
diff |
annotate
|
| Fri, 17 Jan 2014 20:20:20 +0100 |
wenzelm |
clarified @{rail} syntax: prefer explicit \<newline> symbol;
|
file |
diff |
annotate
|
| Wed, 15 Jan 2014 23:25:28 +0100 |
wenzelm |
added \<newline> symbol, which is used for char/string literals in HOL;
|
file |
diff |
annotate
|
| Mon, 13 Jan 2014 20:20:44 +0100 |
wenzelm |
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
|
file |
diff |
annotate
|
| Mon, 13 Jan 2014 18:47:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 12 Jan 2014 18:40:49 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 12:57:26 +0100 |
wenzelm |
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:48 +0100 |
haftmann |
fundamental treatment of undefined vs. universally partial replaces code_abort
|
file |
diff |
annotate
|
| Mon, 30 Dec 2013 20:35:17 +0100 |
wenzelm |
added system option "jedit_print_mode";
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:07 +0100 |
haftmann |
abolished slightly odd global lattice interpretation for min/max
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 16:16:36 +0100 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Tue, 17 Dec 2013 11:12:10 +0100 |
immler |
NEWS
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 15:10:16 +0100 |
haftmann |
disambiguation of interpretation prefixes
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 22:56:28 +0100 |
wenzelm |
discontinued legacy_isub_isup;
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 22:49:27 +0100 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 20:16:12 +0100 |
wenzelm |
provide @{file_unchecked} in Isabelle/Pure;
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 12:16:52 +0100 |
wenzelm |
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2013 23:36:28 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2013 22:10:45 +0100 |
wenzelm |
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
|
file |
diff |
annotate
|
| Thu, 05 Dec 2013 18:02:55 +0100 |
wenzelm |
relocate NEWS to post-release version (cf. 7a14f831d02d);
|
file |
diff |
annotate
|
| Thu, 05 Dec 2013 17:58:03 +0100 |
wenzelm |
merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
|
file |
diff |
annotate
|
| Sun, 01 Dec 2013 17:09:35 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 Nov 2013 17:26:00 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 21:36:10 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 22:13:11 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 23:00:18 +0100 |
wenzelm |
updated to Isabelle2013-2;
|
file |
diff |
annotate
|
| Thu, 05 Dec 2013 13:22:00 +0100 |
blanchet |
make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes
|
file |
diff |
annotate
|
| Thu, 05 Dec 2013 09:23:59 +0100 |
Andreas Lochbihler |
news
|
file |
diff |
annotate
|
| Tue, 26 Nov 2013 09:49:52 +0100 |
traytel |
NEWS
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 18:18:58 +0100 |
haftmann |
even more precise NEWS
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 17:00:49 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 18:14:56 +0100 |
haftmann |
more correct NEWS
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Sat, 16 Nov 2013 17:39:11 +0100 |
wenzelm |
toplevel function "use" refers to raw ML bootstrap environment;
|
file |
diff |
annotate
|
| Mon, 11 Nov 2013 17:44:21 +0100 |
wenzelm |
merged, using src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML and src/HOL/Tools/Sledgehammer/sledgehammer_run.ML from 347c3b0cab44;
|
file |
diff |
annotate
|
| Sat, 09 Nov 2013 11:24:21 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 18:16:16 +0100 |
wenzelm |
no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;
|
file |
diff |
annotate
|
| Wed, 30 Oct 2013 17:05:23 +0100 |
wenzelm |
more on file-system access;
|
file |
diff |
annotate
|
| Mon, 14 Oct 2013 15:21:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 23:11:56 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 04 Oct 2013 13:17:49 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 10 Nov 2013 15:05:06 +0100 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:03 +0100 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 20:10:09 +0100 |
haftmann |
fact generalization and name consolidation
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
purely algebraic foundation for even/odd
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
|
file |
diff |
annotate
|
| Thu, 03 Oct 2013 19:01:10 +0200 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Thu, 03 Oct 2013 00:39:16 +0200 |
ballarin |
Streamlined locales reference material.
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 17:08:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 16:56:02 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 15:53:20 +0200 |
traytel |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 10:13:54 +0300 |
kuncar |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Tue, 01 Oct 2013 14:29:27 +0200 |
blanchet |
minor textual changes
|
file |
diff |
annotate
|
| Sun, 29 Sep 2013 12:56:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 29 Sep 2013 12:44:40 +0200 |
wenzelm |
more on text completion;
|
file |
diff |
annotate
|
| Sat, 28 Sep 2013 16:10:26 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Sat, 28 Sep 2013 14:36:04 +0200 |
wenzelm |
uniform $ISABELLE_HOME on all platforms;
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 16:29:35 +0200 |
wenzelm |
updated documentation concerning MacOSX plugin 1.3;
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 20:24:14 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
document "spy"
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
document "spy" option
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 18:59:28 +0200 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 01:15:26 +0200 |
blanchet |
updated NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 13:18:51 +0200 |
wenzelm |
improved printing of exception trace in Poly/ML 5.5.1;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2013 15:18:14 +0200 |
lammich |
order_bot, order_top
|
file |
diff |
annotate
|
| Tue, 17 Sep 2013 13:40:44 +0200 |
noschinl |
NEWS: Simps_Case_Conv
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 11:46:24 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Fri, 13 Sep 2013 09:31:45 +0200 |
krauss |
merged
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 20:34:32 +0200 |
krauss |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 18:52:30 +0200 |
haftmann |
more correct NEWS
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 11:08:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 02 Sep 2013 17:14:35 +0200 |
Andreas Lochbihler |
NEWS
|
file |
diff |
annotate
|
| Sat, 31 Aug 2013 12:14:19 +0200 |
wenzelm |
more accurate description: Swing/L&F has additional handlers;
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 13:46:32 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 13:45:57 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 12:12:41 +0200 |
blanchet |
renamed command to clarify connection with BNF
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 12:06:37 +0200 |
blanchet |
updated news/contributors with BNF stuff
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 21:49:46 +0200 |
wenzelm |
added action isabelle.complete, using standard jEdit keyboard shortcut;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 10:24:43 +0200 |
wenzelm |
some completion options;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 09:16:03 +0200 |
wenzelm |
GTK+ works better due to avoidance of default list view popups;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 22:25:14 +0200 |
wenzelm |
complete symbols only in backslash forms -- less intrusive editing, greater chance of finding escape sequence in text;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 12:40:55 +0200 |
wenzelm |
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 11:44:28 +0200 |
wenzelm |
obsolete (see 52790e3961fe);
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 11:41:17 +0200 |
wenzelm |
added action isabelle.reset-font-size;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 11:23:26 +0200 |
wenzelm |
tuned -- some reformatting;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 11:39:53 +0200 |
krauss |
renamed theory Mrec to Legacy_Mrec, no longer included by default
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 12:25:26 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 20:34:46 +0200 |
wenzelm |
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 17:26:22 +0200 |
wenzelm |
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 20:31:51 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 15:35:33 +0200 |
wenzelm |
more NEWS and CONTRIBUTORS;
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 21:53:33 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 10:54:37 +0200 |
wenzelm |
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 20:46:21 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 22:20:25 +0200 |
wenzelm |
discontinued historic document formats;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 22:16:04 +0200 |
wenzelm |
avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 21:43:12 +0200 |
wenzelm |
discontinued ISABELLE_DOC_FORMAT;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 21:02:41 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 14:13:34 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 17:53:58 +0200 |
haftmann |
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 18:43:14 +0200 |
wenzelm |
discontinued obsolete "isabelle print";
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 18:34:29 +0200 |
wenzelm |
discontinued command 'print_drafts';
|
file |
diff |
annotate
|
| Sat, 06 Jul 2013 21:19:38 +0200 |
wenzelm |
minimal jedit mode for Isabelle NEWS;
|
file |
diff |
annotate
|
| Sun, 30 Jun 2013 12:30:02 +0200 |
wenzelm |
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
|
file |
diff |
annotate
|
| Sun, 30 Jun 2013 11:37:34 +0200 |
wenzelm |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 23:17:26 +0200 |
wenzelm |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 10:35:37 +0200 |
wenzelm |
updated documentation;
|
file |
diff |
annotate
|
| Tue, 25 Jun 2013 16:55:10 +0200 |
wenzelm |
dockable window for Isabelle documentation;
|
file |
diff |
annotate
|
| Mon, 24 Jun 2013 23:33:14 +0200 |
wenzelm |
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:23:36 +0200 |
wenzelm |
proper diagnostic command 'print_state';
|
file |
diff |
annotate
|
| Tue, 18 Jun 2013 15:31:52 +0200 |
wenzelm |
eliminated old "ref" manual;
|
file |
diff |
annotate
|
| Sat, 15 Jun 2013 17:19:23 +0200 |
haftmann |
lifting for primitive definitions;
|
file |
diff |
annotate
|
| Sun, 02 Jun 2013 07:46:40 +0200 |
haftmann |
make reification part of HOL
|
file |
diff |
annotate
|
| Fri, 31 May 2013 07:30:23 +0200 |
bulwahn |
NEWS about Spec_Check
|
file |
diff |
annotate
|
| Sat, 25 May 2013 18:30:38 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:44:29 +0200 |
haftmann |
weaker precendence of syntax for big intersection and union on sets
|
file |
diff |
annotate
|
| Wed, 22 May 2013 18:10:54 +0200 |
wenzelm |
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:53:28 +0200 |
wenzelm |
renamed 'print_configs' to 'print_options';
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 18:39:49 +0200 |
wenzelm |
discontinued obsolete isabelle-process options -f and -u;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 18:23:39 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 18:19:42 +0200 |
wenzelm |
discontinued obsolete isabelle usedir, mkdir, make;
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 11:59:21 +0200 |
hoelzl |
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 10:35:56 +0200 |
hoelzl |
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 13:28:30 +0200 |
hoelzl |
spell conditional_ly_-complete lattices correct
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 19:31:24 +0200 |
haftmann |
documentation and NEWS
|
file |
diff |
annotate
|
| Mon, 22 Apr 2013 16:36:02 +0200 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Fri, 12 Apr 2013 17:21:51 +0200 |
wenzelm |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 19:14:47 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 17:02:47 +0200 |
wenzelm |
added ML antiquotation @{theory_context};
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 17:49:16 +0200 |
traytel |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Tue, 02 Apr 2013 16:29:40 +0200 |
wenzelm |
NEWS for 635562bc14ef;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 22:36:03 +0100 |
ballarin |
Improvements to the print_dependencies command.
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 16:38:25 +0100 |
wenzelm |
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 11:26:13 +0100 |
wenzelm |
dockable window for timing information;
|
file |
diff |
annotate
|
| Mon, 25 Mar 2013 20:00:27 +0100 |
ballarin |
Discontinued theories src/HOL/Algebra/abstract and .../poly.
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:57:57 +0100 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 17:11:06 +0100 |
haftmann |
locales for abstract orders
|
file |
diff |
annotate
|
| Wed, 13 Mar 2013 15:12:14 +0100 |
wenzelm |
sessions may be organized via 'chapter' in ROOT;
|
file |
diff |
annotate
|
| Tue, 12 Mar 2013 16:47:24 +0100 |
wenzelm |
discontinued "isabelle usedir" option -r (reset session path);
|
file |
diff |
annotate
|
| Mon, 11 Mar 2013 14:25:14 +0100 |
wenzelm |
discontinued "isabelle usedir" option -P (remote path);
|
file |
diff |
annotate
|
| Sat, 09 Mar 2013 11:56:01 +0100 |
haftmann |
discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 17:38:35 +0100 |
wenzelm |
discontinued empty name bindings in 'axiomatization';
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 16:38:17 +0100 |
wenzelm |
discontinued obsolete 'axioms' command;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 17:32:17 +0100 |
wenzelm |
discontinued redundant 'use' command;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 12:45:19 +0100 |
wenzelm |
discontinued obsolete 'uses' within theory header;
|
file |
diff |
annotate
|
| Fri, 22 Feb 2013 14:25:52 +0100 |
wenzelm |
discontinued obsolete src/HOL/IsaMakefile;
|
file |
diff |
annotate
|
| Sat, 16 Feb 2013 08:21:08 +0100 |
haftmann |
restored proper order of NEWS entries (lost due too long-waiting patches)
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 14:14:55 +0100 |
haftmann |
consolidation of library theories on product orders
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 11:46:48 +0100 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Sun, 10 Feb 2013 14:57:00 +0100 |
wenzelm |
updated PIDE notes;
|
file |
diff |
annotate
|
| Mon, 28 Jan 2013 12:22:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 26 Jan 2013 13:49:48 +0100 |
wenzelm |
clarified NEWS on isabelle build and mkroot;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2013 15:28:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:42:12 +0100 |
hoelzl |
remove unnecessary assumption from real_normed_vector
|
file |
diff |
annotate
|
| Sun, 20 Jan 2013 15:34:27 +0100 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Sun, 20 Jan 2013 15:26:56 +0100 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| Sun, 20 Jan 2013 14:00:05 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 14:03:24 +0100 |
kuncar |
NEWS
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 22:01:49 +0100 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Wed, 09 Jan 2013 12:22:09 +0100 |
wenzelm |
tune spelling;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 16:23:07 +0100 |
wenzelm |
allow negative argument in "consumes" source format;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 21:24:47 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 21:16:08 +0100 |
wenzelm |
more reactive completion popup by default;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 19:00:49 +0100 |
blanchet |
updated docs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 13:03:21 +0100 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 12:44:47 +0100 |
wenzelm |
document 'locale_deps';
|
file |
diff |
annotate
|
| Thu, 03 Jan 2013 14:23:10 +0100 |
wenzelm |
NEWS: ML runtime statistics;
|
file |
diff |
annotate
|
| Mon, 31 Dec 2012 13:08:37 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Mon, 31 Dec 2012 12:25:11 +0100 |
wenzelm |
recovered Isabelle2012 NEWS from ae12b92c145a, except for e5420161d11d;
|
file |
diff |
annotate
|
| Sat, 29 Dec 2012 17:18:01 +0100 |
nipkow |
new theory Library/Finite_Lattice
|
file |
diff |
annotate
|
| Sun, 23 Dec 2012 19:54:15 +0100 |
nipkow |
renamed and added lemmas
|
file |
diff |
annotate
|
| Tue, 18 Dec 2012 21:59:44 +0100 |
haftmann |
discontinued legacy antiquotations and styles
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 15:46:01 +0100 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 14:46:01 +0100 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 12:40:07 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 13:11:38 +0100 |
Christian Sternagel |
renamed "emb" to "list_hembeq";
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 19:53:55 +0100 |
wenzelm |
smarter handling of tracing messages: prover process pauses and enters user dialog;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 16:06:57 +0100 |
wenzelm |
more generous tracing limit -- rescaled in MB;
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 21:46:20 +0100 |
wenzelm |
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 19:53:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 17:13:44 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 11:46:19 +0100 |
blanchet |
updated NEWS etc.
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 13:54:43 +0100 |
wenzelm |
refined outer syntax 'help' command;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 17:15:21 +0100 |
wenzelm |
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 15:49:43 +0100 |
wenzelm |
more NEWS/CONTRIBUTORS;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 14:50:19 +0100 |
wenzelm |
improved editing support for control styles;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 12:39:58 +0100 |
wenzelm |
added ISABELLE_PLATFORM_FAMILY;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 10:57:50 +0100 |
hoelzl |
NEWS: document changes in HOL-Probability
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 10:48:58 +0100 |
hoelzl |
NEWS (changeset 13211e07d931): add Countable_Set
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 10:48:22 +0100 |
hoelzl |
NEWS (changeset 69b35a75caf3): document changes in FuncSet
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 09:07:41 +0100 |
nipkow |
new theory of immutable arrays
|
file |
diff |
annotate
|
| Tue, 20 Nov 2012 15:18:11 +0100 |
wenzelm |
simplified command line of "isabelle install";
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 16:04:13 +0100 |
wenzelm |
more generous tracing_limit, with explicit system option;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 15:38:37 +0100 |
wenzelm |
adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
|
file |
diff |
annotate
|
| Sat, 17 Nov 2012 20:19:34 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2012 19:55:19 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Tue, 06 Nov 2012 15:15:33 +0100 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 22:24:34 +0200 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
file |
diff |
annotate
|