src/Doc/Isar_Ref/Proof.thy
Wed, 21 Oct 2015 00:23:11 +0200 wenzelm proper spaces around @{text};
Tue, 20 Oct 2015 23:53:40 +0200 wenzelm isabelle update_cartouches -t;
Sun, 18 Oct 2015 22:57:09 +0200 wenzelm more control symbols;
Fri, 16 Oct 2015 14:53:26 +0200 wenzelm Markdown support in document text;
Wed, 14 Oct 2015 15:10:32 +0200 wenzelm more symbols;
Mon, 12 Oct 2015 22:03:24 +0200 wenzelm more symbols;
Mon, 12 Oct 2015 19:32:25 +0200 wenzelm @{verbatim [display]} supersedes old alltt/ttbox;
Tue, 06 Oct 2015 15:39:00 +0200 wenzelm added 'proposition' command;
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
Sun, 13 Sep 2015 20:20:16 +0200 wenzelm renamed method "goals" to "goal_cases" to emphasize its meaning;
Sun, 13 Sep 2015 14:44:03 +0200 wenzelm method "goals" ignores facts;
Tue, 30 Jun 2015 15:20:56 +0200 wenzelm renamed "default" to "standard", to make semantically clear what it is;
Thu, 25 Jun 2015 21:45:00 +0200 wenzelm added method "goals" for proper subgoal cases;
Wed, 24 Jun 2015 21:26:03 +0200 wenzelm clarified 'case' command;
Mon, 22 Jun 2015 20:36:33 +0200 wenzelm support 'when' statement, which corresponds to 'presume';
Mon, 15 Jun 2015 14:10:41 +0200 wenzelm moved sections;
Mon, 15 Jun 2015 13:29:57 +0200 wenzelm moved sections;
Mon, 15 Jun 2015 10:38:09 +0200 wenzelm tuned;
Mon, 15 Jun 2015 10:25:49 +0200 wenzelm tuned;
Sat, 13 Jun 2015 22:42:23 +0200 wenzelm more on 'consider' and related concepts;
Sat, 13 Jun 2015 17:14:05 +0200 wenzelm implicit rule for method "cases";
Sat, 13 Jun 2015 13:09:05 +0200 wenzelm renamed "prems" to "that";
Thu, 11 Jun 2015 22:47:53 +0200 wenzelm support for 'consider' command;
Wed, 10 Jun 2015 14:46:31 +0200 wenzelm support for "if prems" in local goal statements;
Tue, 09 Jun 2015 16:07:11 +0200 wenzelm allow for_fixes for 'have', 'show' etc.;
Fri, 05 Jun 2015 13:41:06 +0200 wenzelm added Isar command 'supply';
Sat, 18 Apr 2015 20:46:48 +0200 wenzelm tuned;
Sat, 18 Apr 2015 20:44:55 +0200 wenzelm clarified syntax diagram: 'obtains' does not allow prop_pat (although it could and should at some point);
Thu, 09 Apr 2015 22:53:26 +0200 wenzelm make SML/NJ more happy;
Wed, 01 Apr 2015 23:59:56 +0200 wenzelm misc tuning -- keep name space more clean;
Mon, 30 Mar 2015 14:19:45 +0200 wenzelm more uniform syntax for named instantiations;
Mon, 23 Mar 2015 17:07:43 +0100 wenzelm tuned;
Mon, 23 Mar 2015 17:01:47 +0100 wenzelm clarified syntax category "fixes";
Mon, 23 Mar 2015 15:55:41 +0100 wenzelm tuned syntax diagrams -- no duplication of "target";
Mon, 09 Mar 2015 20:33:33 +0100 wenzelm support structural composition (THEN_ALL_NEW) for proof methods;
Tue, 07 Oct 2014 21:44:41 +0200 wenzelm clarified whitespace;
Tue, 07 Oct 2014 21:29:59 +0200 wenzelm more cartouches;
Sun, 05 Oct 2014 22:24:07 +0200 wenzelm prefer @{cite} antiquotation;
Mon, 18 Aug 2014 13:19:04 +0200 wenzelm merged;
Wed, 13 Aug 2014 20:08:29 +0200 wenzelm tuned;
Sat, 16 Aug 2014 12:15:56 +0200 wenzelm updated syntax for localized commands;
Thu, 14 Aug 2014 14:28:11 +0200 wenzelm localized command 'method_setup' and 'attribute_setup';
Tue, 15 Apr 2014 00:21:31 +0200 wenzelm tuned spelling;
Tue, 08 Apr 2014 12:46:38 +0200 haftmann even more standardized doc session names after #b266e7a86485
less more (0) tip