| Wed, 14 Sep 2016 14:37:38 +0200 |
wenzelm |
discontinued global etc/abbrevs;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 13:26:14 +0200 |
wenzelm |
strictly sequential abbrevs;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 17:35:18 +0200 |
wenzelm |
support 'abbrevs' within theory header;
|
file |
diff |
annotate
|
| Sat, 16 Jul 2016 00:38:33 +0200 |
wenzelm |
information about proof outline with cases (sendback);
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 23:46:28 +0200 |
wenzelm |
singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 20:58:00 +0200 |
wenzelm |
clarified indentation;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 16:36:29 +0200 |
wenzelm |
explicit kind "before_command";
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 10:43:54 +0200 |
wenzelm |
more indentation for quasi_command keywords;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2016 17:35:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:41:11 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 22:47:25 +0200 |
wenzelm |
added command 'unbundle';
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 12:45:34 +0200 |
wenzelm |
prefer hybrid 'bundle' command;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 17:13:52 +0200 |
wenzelm |
clarified;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 15:41:49 +0200 |
wenzelm |
support for bundle definition via target;
|
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
|
| Sat, 14 May 2016 19:49:10 +0200 |
wenzelm |
toplevel theorem statements support 'if'/'for' eigen-context;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
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, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Sun, 10 Apr 2016 21:46:12 +0200 |
wenzelm |
more standard session build process, including browser_info;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 16:53:43 +0200 |
wenzelm |
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 12:13:11 +0200 |
wenzelm |
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 18:20:25 +0200 |
wenzelm |
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 15:53:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 23:58:48 +0200 |
wenzelm |
more uniform ML file commands;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 23:08:43 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 22:13:08 +0200 |
wenzelm |
tuned -- more explicit sections;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 17:25:53 +0200 |
wenzelm |
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 17:02:34 +0200 |
wenzelm |
clarified bootstrap -- more uniform use of ML files;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 19:42:59 +0100 |
wenzelm |
ML debugger support in Pure (again, see 3565c9f407ec);
|
file |
diff |
annotate
|
| Sun, 14 Feb 2016 16:30:27 +0100 |
wenzelm |
command '\<proof>' is an alias for 'sorry', with different typesetting;
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 16:55:56 +0100 |
wenzelm |
removed old 'defs' command;
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 11:05:04 +0100 |
haftmann |
abandoned attempt to unify sublocale and interpretation into global theories
|
file |
diff |
annotate
|
| Wed, 16 Dec 2015 16:31:36 +0100 |
wenzelm |
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 08:45:52 +0100 |
haftmann |
prefer "rewrites" and "defines" to note rewrite morphisms
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 08:45:52 +0100 |
haftmann |
coalesce permanent_interpretation.ML with interpretation.ML
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 20:10:17 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 00:02:30 +0100 |
wenzelm |
symbolic syntax "\<comment> text";
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
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
|
| Tue, 22 Sep 2015 18:56:25 +0200 |
wenzelm |
separate command 'print_definitions';
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 19:34:15 +0200 |
wenzelm |
support for ML files with/without debugger information;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2015 21:40:47 +0200 |
wenzelm |
skeleton for interactive debugger;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 15:37:32 +0200 |
wenzelm |
clarified text folds: proof ... qed counts as extra block;
|
file |
diff |
annotate
|
| Wed, 01 Jul 2015 21:48:46 +0200 |
wenzelm |
clarified keyword categories;
|
file |
diff |
annotate
|
| Wed, 01 Jul 2015 21:29:57 +0200 |
wenzelm |
support for subgoal focus command;
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 20:36:33 +0200 |
wenzelm |
support 'when' statement, which corresponds to 'presume';
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 22:47:53 +0200 |
wenzelm |
support for 'consider' command;
|
file |
diff |
annotate
|
| Fri, 05 Jun 2015 13:41:06 +0200 |
wenzelm |
added Isar command 'supply';
|
file |
diff |
annotate
|
| Sat, 30 May 2015 22:18:12 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 13:48:10 +0200 |
wenzelm |
clarified thy_deps;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 14:04:11 +0200 |
wenzelm |
support private scope for individual local theory commands;
|
file |
diff |
annotate
|