| Sat, 17 Mar 2012 22:46:19 +0100 |
more precise syntax;
|
file | diff | annotate |
| Sun, 20 Nov 2011 17:44:41 +0100 |
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
|
file | diff | annotate |
| Mon, 06 Jun 2011 22:02:34 +0200 |
tuned;
|
file | diff | annotate |
| Sun, 15 May 2011 17:06:35 +0200 |
optional description for 'attribute_setup' and 'method_setup';
|
file | diff | annotate |
| Thu, 05 May 2011 23:23:02 +0200 |
tuned some syntax names;
|
file | diff | annotate |
| Thu, 05 May 2011 23:15:11 +0200 |
tuned rail diagrams and layout;
|
file | diff | annotate |
| Tue, 03 May 2011 15:07:36 +0200 |
formal Base theory;
|
file | diff | annotate |
| Mon, 02 May 2011 20:34:34 +0200 |
eliminated some duplicate "def" positions;
|
file | diff | annotate |
| Mon, 02 May 2011 20:14:19 +0200 |
'axiomatization' is global;
|
file | diff | annotate |
| Mon, 02 May 2011 17:06:40 +0200 |
more precise rail diagrams;
|
file | diff | annotate |
| Mon, 02 May 2011 01:05:50 +0200 |
modernized rail diagrams using @{rail} antiquotation;
|
file | diff | annotate |
| Thu, 06 Jan 2011 21:06:18 +0100 |
Diagnostic command to show locale dependencies.
|
file | diff | annotate |
| Thu, 06 Jan 2011 21:06:17 +0100 |
Documentation for 'interpret' and 'sublocale' with mixins.
|
file | diff | annotate |
| Fri, 17 Dec 2010 18:10:37 +0100 |
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
|
file | diff | annotate |
| Sun, 28 Nov 2010 21:07:28 +0100 |
Parse.liberal_name for document antiquotations and attributes;
|
file | diff | annotate |
| Sun, 28 Nov 2010 16:15:31 +0100 |
added 'syntax_declaration' command;
|
file | diff | annotate |
| Fri, 29 Oct 2010 16:16:10 +0200 |
eliminated obsolete \_ escape;
|
file | diff | annotate |
| Fri, 29 Oct 2010 11:49:56 +0200 |
eliminated obsolete \_ escapes in rail environments;
|
file | diff | annotate |
| Thu, 28 Oct 2010 22:59:33 +0200 |
tuned;
|
file | diff | annotate |
| Thu, 28 Oct 2010 22:39:59 +0200 |
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
|
file | diff | annotate |
| Sun, 24 Oct 2010 21:25:13 +0200 |
merged
|
file | diff | annotate |
| Fri, 15 Oct 2010 19:19:41 +0100 |
moved bind_thm(s) to implementation manual;
|
file | diff | annotate |
| Sat, 09 Oct 2010 19:49:19 +0100 |
prefer checked antiquotations;
|
file | diff | annotate |
| Sun, 10 Oct 2010 23:16:24 +0200 |
do not mention unqualified names, now that 'global' and 'local' are gone
|
file | diff | annotate |
| Wed, 08 Sep 2010 13:22:24 +0200 |
removed ancient constdefs command
|
file | diff | annotate |
| Wed, 25 Aug 2010 14:18:09 +0200 |
discontinued obsolete 'global' and 'local' commands;
|
file | diff | annotate |
| Sat, 31 Jul 2010 23:32:05 +0200 |
Documentation of 'interpret' updated.
|
file | diff | annotate |
| Mon, 12 Jul 2010 11:21:27 +0200 |
moved co-regularity to class section; avoid duplicated class_deps
|
file | diff | annotate |
| Mon, 24 May 2010 21:18:22 +0100 |
Typo fixed.
|
file | diff | annotate |
| Wed, 28 Apr 2010 12:21:55 +0200 |
command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
|
file | diff | annotate |
| Fri, 16 Apr 2010 22:18:59 +0200 |
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
|
file | diff | annotate |
| Fri, 16 Apr 2010 22:15:09 +0200 |
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
|
file | diff | annotate |
| Tue, 09 Mar 2010 23:32:13 +0100 |
localized typedecl;
|
file | diff | annotate |
| Wed, 24 Feb 2010 20:37:01 +0100 |
allow general mixfix syntax for type constructors;
|
file | diff | annotate |
| Mon, 22 Feb 2010 17:02:39 +0100 |
dropped references to old axclass from documentation
|
file | diff | annotate |
| Mon, 23 Nov 2009 21:03:49 +0100 |
Typos in documenation.
|
file | diff | annotate |
| Sun, 22 Nov 2009 15:37:14 +0100 |
Updated locale documentation.
|
file | diff | annotate |
| Sun, 08 Nov 2009 14:44:31 +0100 |
added "declaration (pervasive)";
|
file | diff | annotate |
| Thu, 02 Jul 2009 16:06:12 +0200 |
instance arities can be simultaneous
|
file | diff | annotate |
| Wed, 17 Jun 2009 10:34:02 +0200 |
refined section concerning classes
|
file | diff | annotate |
| Wed, 06 May 2009 16:01:05 +0200 |
tuned description of overloading
|
file | diff | annotate |
| Mon, 16 Mar 2009 17:48:02 +0100 |
spelling;
|
file | diff | annotate |
| Sun, 15 Mar 2009 15:59:43 +0100 |
added 'attribute_setup' command;
|
file | diff | annotate |
| Wed, 11 Mar 2009 23:59:34 +0100 |
added 'local_setup' command;
|
file | diff | annotate |
| Wed, 04 Mar 2009 11:05:29 +0100 |
Merge.
|
file | diff | annotate |
| Wed, 04 Mar 2009 10:45:52 +0100 |
Merge.
|
file | diff | annotate |
| Mon, 16 Feb 2009 20:15:40 +0100 |
modernized some theory names;
|
file | diff | annotate |
| Sun, 15 Feb 2009 18:54:50 +0100 |
added introduction;
|
file | diff | annotate |
| Mon, 02 Feb 2009 09:27:54 +0100 |
updated type class section
|
file | diff | annotate |
| Thu, 22 Jan 2009 09:04:45 +0100 |
dropped print_interps
|
file | diff | annotate |
| Mon, 19 Jan 2009 13:37:24 +0100 |
"code equation" replaces "defining equation"
|
file | diff | annotate |
| Thu, 13 Nov 2008 22:44:40 +0100 |
removed "includes" element (lost update?);
|
file | diff | annotate |
| Thu, 13 Nov 2008 21:53:54 +0100 |
added section "Co-regularity of type classes and arities" (variant from old ref manual);
|
file | diff | annotate |
| Thu, 13 Nov 2008 21:52:59 +0100 |
minor tuning (according to old ref manual);
|
file | diff | annotate |
| Thu, 13 Nov 2008 21:48:19 +0100 |
separate chapter "Inner syntax --- the term language";
|
file | diff | annotate |
| Thu, 13 Nov 2008 21:45:40 +0100 |
updated/refined types of Isar language elements, removed special LaTeX macros;
|
file | diff | annotate |
| Thu, 13 Nov 2008 21:43:46 +0100 |
unified use of declaration environment with IsarImplementation;
|
file | diff | annotate |
| Thu, 13 Nov 2008 21:40:30 +0100 |
added bind_thm, bind_thms;
|
file | diff | annotate |
| Thu, 13 Nov 2008 21:40:00 +0100 |
tuned section "Incorporating ML code";
|
file | diff | annotate |
| Thu, 13 Nov 2008 21:38:44 +0100 |
tuned section "Oracles";
|
file | diff | annotate |