| 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
|