| Tue, 01 Dec 2015 12:35:11 +0100 |
Andreas Lochbihler |
add formalisation of Bourbaki-Witt fixpoint theorem
|
file |
diff |
annotate
|
| Wed, 25 Nov 2015 15:58:22 +0100 |
wenzelm |
observe option "indent";
|
file |
diff |
annotate
|
| Sun, 22 Nov 2015 13:33:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 21 Nov 2015 20:19:20 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 18 Nov 2015 21:18:33 +0100 |
ballarin |
Refine the supression of abbreviations for morphisms that are not identities.
|
file |
diff |
annotate
|
| Tue, 17 Nov 2015 12:32:08 +0000 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
file |
diff |
annotate
|
| Mon, 16 Nov 2015 12:37:46 +0100 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| Sun, 15 Nov 2015 13:49:27 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 15 Nov 2015 12:39:51 +0100 |
wenzelm |
option "inductive_defs" controls exposure of def and mono facts;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2015 10:51:22 +0100 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 17:37:44 +0100 |
haftmann |
represent both algebraic and local-theory views on locale interpretation in interfaces
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 08:45:52 +0100 |
haftmann |
coalesce permanent_interpretation.ML with interpretation.ML
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 19:59:28 +0100 |
wenzelm |
added antiquotation @{doc}, e.g. useful for demonstration purposes;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 16:02:59 +0100 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2015 11:30:56 +0100 |
wenzelm |
support short form for \<^theory_text>;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 09:21:56 +0100 |
Andreas Lochbihler |
cancel complementary terms as arguments to sup/inf in boolean algebras
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 23:21:02 +0100 |
wenzelm |
added @{command}, @{method}, @{attribute};
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 19:03:29 +0100 |
wenzelm |
added document antiquotation @{theory_text};
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 21:04:49 +0100 |
wenzelm |
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 13:49:56 +0100 |
wenzelm |
prefer explicit State panel;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2015 14:41:07 +0100 |
wenzelm |
added option timeout_scale;
|
file |
diff |
annotate
|
| Sat, 07 Nov 2015 16:05:28 +0100 |
wenzelm |
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
|
file |
diff |
annotate
|
| Sat, 07 Nov 2015 12:53:22 +0100 |
wenzelm |
added @{undefined} with somewhat undefined symbol;
|
file |
diff |
annotate
|
| Fri, 06 Nov 2015 23:31:50 +0100 |
wenzelm |
more formal treatment of control symbols;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 00:02:30 +0100 |
wenzelm |
symbolic syntax "\<comment> text";
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 18:14:28 +0100 |
wenzelm |
document antiquotation @{footnote};
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 11:53:22 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:49 +0100 |
ballarin |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 21:58:38 +0100 |
blanchet |
don't pollute local theory with needless names
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 21:49:49 +0100 |
blanchet |
allow selectors and discriminators with same name as type
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 10:20:27 +0100 |
wenzelm |
clarified completion of Isabelle symbols within document source;
|
file |
diff |
annotate
|
| Sat, 31 Oct 2015 14:38:48 +0100 |
wenzelm |
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2015 15:17:02 +0000 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
| Sat, 24 Oct 2015 13:42:31 +0200 |
wenzelm |
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2015 19:23:14 +0200 |
wenzelm |
rendering for \<^verbatim>;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2015 00:23:11 +0200 |
wenzelm |
proper spaces around @{text};
|
file |
diff |
annotate
|
| Tue, 20 Oct 2015 23:03:46 +0200 |
wenzelm |
added isabelle update_cartouches option -t;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2015 20:45:33 +0200 |
wenzelm |
another antiquotation short form: undecorated cartouche as alias for @{text};
|
file |
diff |
annotate
|
| Mon, 19 Oct 2015 20:31:13 +0200 |
wenzelm |
tuned English;
|
file |
diff |
annotate
|
| Mon, 19 Oct 2015 16:37:45 +0200 |
wenzelm |
added action "isabelle-emph";
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 20:28:29 +0200 |
wenzelm |
clarified control antiquotations: decode control symbol to get name;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 17:24:24 +0200 |
wenzelm |
support control symbol antiquotations;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 21:15:10 +0200 |
wenzelm |
added 'paragraph', 'subparagraph';
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 19:47:34 +0200 |
wenzelm |
more explicit output of list items;
|
file |
diff |
annotate
|
| Wed, 14 Oct 2015 14:21:00 +0200 |
wenzelm |
clarified control symbols;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 12:42:08 +0100 |
paulson |
new material on path_component_sets, inside, outside, etc. And more default simprules
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Mon, 12 Oct 2015 17:10:36 +0200 |
wenzelm |
some control symbols for markup and formatting;
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 19:22:05 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 21:20:43 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 01:44:29 +0200 |
kuncar |
NEWS
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 18:44:07 +0200 |
blanchet |
news
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 15:39:00 +0200 |
wenzelm |
added 'proposition' command;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 15:14:28 +0200 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 16:14:33 +0200 |
blanchet |
avoid too aggressive optimization of 'finite' predicate
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 15:57:25 +0200 |
blanchet |
avoid unsound simplification of (C (s x)) when s is a selector but not C's
|
file |
diff |
annotate
|
| Sat, 03 Oct 2015 17:11:04 +0200 |
blanchet |
speed up MaSh
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 21:31:51 +0200 |
blanchet |
updated docs and NEWS
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 19:34:12 +0200 |
wenzelm |
avoid useless empty case_names;
|
file |
diff |
annotate
|