| Sat, 08 Dec 2007 22:28:27 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Sat, 08 Dec 2007 21:41:30 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 22:19:49 +0100 |
wenzelm |
added nested 'Isabelle.command';
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:15:51 +0100 |
haftmann |
improved
|
file |
diff |
annotate
|
| Mon, 03 Dec 2007 16:04:17 +0100 |
haftmann |
overloading target
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 16:44:20 +0100 |
wenzelm |
ObjectLogic.typedecl;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:42 +0100 |
haftmann |
tuned interfaces of class module
|
file |
diff |
annotate
|
| Fri, 23 Nov 2007 21:09:35 +0100 |
haftmann |
rudimentary instantiation target
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 20:50:43 +0100 |
wenzelm |
TheoryTarget.context;
|
file |
diff |
annotate
|
| Fri, 02 Nov 2007 18:53:00 +0100 |
haftmann |
clarified theory target interface
|
file |
diff |
annotate
|
| Thu, 25 Oct 2007 16:57:57 +0200 |
wenzelm |
made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 23:21:11 +0200 |
wenzelm |
sorry: proper command;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 14:42:31 +0200 |
haftmann |
dropped local_syntax
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 16:05:26 +0200 |
wenzelm |
renamed Syntax.XXX_mode to Syntax.mode_XXX;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 00:28:30 +0200 |
wenzelm |
'notation': allow 'structure' as well;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:31:58 +0200 |
wenzelm |
added 'no_notation';
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 19:48:54 +0200 |
wenzelm |
class: print result is for locale;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 17:10:45 +0200 |
wenzelm |
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 22:03:21 +0200 |
haftmann |
added proper subclass concept; improved class target
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 17:46:51 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:08 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:15 +0200 |
haftmann |
distinction between regular and default code theorems
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:44 +0200 |
haftmann |
clarified class interfaces and internals
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 18:01:37 +0200 |
berghofe |
Specification.theorem now also takes "interactive" flag as argument.
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:20 +0200 |
haftmann |
overloaded definitions accompanied by explicit constants
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 23:10:46 +0200 |
wenzelm |
removed obsolete touch_all_thys;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|