| Mon, 30 May 2016 20:58:54 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
| Sat, 28 May 2016 21:38:58 +0200 |
wenzelm |
clarified 'axiomatization';
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:43:18 +0200 |
haftmann |
explicit check that abstract constructors cannot be part of official interface
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:43:17 +0200 |
haftmann |
do not export abstract constructors in code_reflect
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:10:48 +0200 |
nipkow |
added subtheory of longest common prefix
|
file |
diff |
annotate
|
| Thu, 26 May 2016 16:57:14 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:31:04 +0200 |
haftmann |
examples and documentation for code generator time measurements
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
delegate inclusion of required dictionaries to user-space instead of half-working magic
|
file |
diff |
annotate
|
| Thu, 26 May 2016 09:05:00 +0200 |
nipkow |
added function "prefixes" and some lemmas
|
file |
diff |
annotate
|
| Wed, 25 May 2016 17:40:56 +0200 |
nipkow |
renamed suffix(eq)
|
file |
diff |
annotate
|
| Wed, 25 May 2016 12:24:00 +0200 |
eberlm |
NEWS: Permutations of a set and randomised folds
|
file |
diff |
annotate
|
| Tue, 24 May 2016 15:16:57 +0200 |
wenzelm |
cartouche abbreviations work both for " as well;
|
file |
diff |
annotate
|
| Tue, 24 May 2016 11:39:26 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 23 May 2016 21:30:30 +0200 |
wenzelm |
embedded content may be delimited via cartouches;
|
file |
diff |
annotate
|
| Mon, 23 May 2016 22:43:22 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Mon, 23 May 2016 22:43:11 +0200 |
nipkow |
renamed prefix* in Library/Sublist
|
file |
diff |
annotate
|
| Mon, 23 May 2016 18:04:45 +0200 |
blanchet |
generate Vampire 4.0 compatible output
|
file |
diff |
annotate
|
| Mon, 23 May 2016 15:30:13 +0200 |
wenzelm |
removed odd cases rule (see also 8cb42cd97579);
|
file |
diff |
annotate
|
| Sat, 14 May 2016 19:49:10 +0200 |
wenzelm |
toplevel theorem statements support 'if'/'for' eigen-context;
|
file |
diff |
annotate
|
| Tue, 10 May 2016 14:04:44 +0100 |
paulson |
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 11:34:26 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 22:39:17 +0200 |
wenzelm |
'obtain' supports structured statements (similar to 'define');
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 19:41:39 +0200 |
wenzelm |
old 'def' is legacy;
|
file |
diff |
annotate
|
| Sun, 24 Apr 2016 21:31:14 +0200 |
wenzelm |
added Isar command 'define';
|
file |
diff |
annotate
|
| Wed, 20 Apr 2016 11:44:25 +0200 |
wenzelm |
reactivated other_id reports (see also db929027e701, 8eda56033203);
|
file |
diff |
annotate
|
| Tue, 19 Apr 2016 12:06:34 +0200 |
wenzelm |
more IDE support for Isabelle/Pure bootstrap;
|
file |
diff |
annotate
|
| Fri, 15 Apr 2016 16:50:23 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 23:31:10 +0200 |
wenzelm |
highlighting of entity def/ref positions wrt. cursor;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:55:00 +0200 |
hoelzl |
change is incompatible
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:48:11 +0200 |
hoelzl |
Probability: move emeasure and nn_integral from ereal to ennreal
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 18:49:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 14:38:57 +0200 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 21:42:42 +0200 |
wenzelm |
removed old proof method "default";
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 19:30:15 +0200 |
wenzelm |
support ROOT0.ML as well -- independently of ROOT.ML;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 17:26:22 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 11:57:21 +0200 |
wenzelm |
simplified bootstrap: critical structures remain accessible in ML_Root context;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 19:41:58 +0200 |
wenzelm |
clarified bootstrap environment;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 23:13:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 20:07:08 +0200 |
wenzelm |
option ML_system_unsafe;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 09:45:04 +0200 |
blanchet |
added reference from NEWS to docs
|
file |
diff |
annotate
|
| Sun, 03 Apr 2016 23:56:52 +0200 |
wenzelm |
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 21:34:51 +0200 |
wenzelm |
documentation;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 16:15:31 +0200 |
wenzelm |
explicit property for unbreakable block;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 12:39:37 +0100 |
blanchet |
document addition of 'corec'
|
file |
diff |
annotate
|
| Sat, 19 Mar 2016 16:53:09 +0100 |
haftmann |
unified CHAR with CHR syntax
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 20:35:01 +0100 |
wenzelm |
recovered from Unicode accident in 7248d106c607;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 20:29:50 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 17 Mar 2016 16:56:44 +0100 |
wenzelm |
@{make_string} is available during Pure bootstrap;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 08:01:49 +0100 |
Andreas Lochbihler |
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 22:19:08 +0100 |
wenzelm |
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 22:04:38 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 22:22:12 +0100 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 22:04:52 +0100 |
haftmann |
model characters directly as range 0..255
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 22:21:01 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 12:11:50 +0100 |
wenzelm |
isabelle_process is superseded by "isabelle process" tool;
|
file |
diff |
annotate
|
| Wed, 09 Mar 2016 21:01:22 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 08 Mar 2016 20:02:46 +0100 |
wenzelm |
back to external line editor, due to problems of JLine with multithreading of in vs. out;
|
file |
diff |
annotate
|
| Tue, 08 Mar 2016 18:15:16 +0100 |
wenzelm |
isabelle console is based on Isabelle/Scala;
|
file |
diff |
annotate
|