src/Doc/Isar_Ref/Proof.thy
18 months ago wenzelm 2017-12-03 discontinued old 'def' command;
2017-01-20 wenzelm 2017-01-20 tuned;
2016-09-07 wenzelm 2016-09-07 unfold_abs_def is enabled by default;
2016-07-20 wenzelm 2016-07-20 clarified imports; tuned;
2016-07-20 wenzelm 2016-07-20 oops;
2016-07-20 wenzelm 2016-07-20 moved method "use" to Pure; more documentation;
2016-06-11 wenzelm 2016-06-11 clarified syntax;
2016-05-14 wenzelm 2016-05-14 toplevel theorem statements support 'if'/'for' eigen-context;
2016-04-26 wenzelm 2016-04-26 'obtain' supports structured statements (similar to 'define');
2016-04-24 wenzelm 2016-04-24 added Isar command 'define';
2016-04-18 wenzelm 2016-04-18 prefer internal attribute source;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-02-10 wenzelm 2016-02-10 tuned;
2016-02-07 wenzelm 2016-02-07 clarified old forms;
2015-11-13 wenzelm 2015-11-13 more documentation;
2015-11-13 wenzelm 2015-11-13 tuned whitespace;
2015-11-13 wenzelm 2015-11-13 more uniform jEdit properties;
2015-11-04 wenzelm 2015-11-04 more antiquotations;
2015-10-22 wenzelm 2015-10-22 more control symbols; tuned;
2015-10-21 wenzelm 2015-10-21 proper spaces around @{text};
2015-10-20 wenzelm 2015-10-20 isabelle update_cartouches -t;
2015-10-18 wenzelm 2015-10-18 more control symbols;
2015-10-16 wenzelm 2015-10-16 Markdown support in document text;
2015-10-14 wenzelm 2015-10-14 more symbols;
2015-10-12 wenzelm 2015-10-12 more symbols;
2015-10-12 wenzelm 2015-10-12 @{verbatim [display]} supersedes old alltt/ttbox;
2015-10-06 wenzelm 2015-10-06 added 'proposition' command;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-09-13 wenzelm 2015-09-13 renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-09-13 wenzelm 2015-09-13 method "goals" ignores facts;
2015-06-30 wenzelm 2015-06-30 renamed "default" to "standard", to make semantically clear what it is;
2015-06-25 wenzelm 2015-06-25 added method "goals" for proper subgoal cases;
2015-06-24 wenzelm 2015-06-24 clarified 'case' command;
2015-06-22 wenzelm 2015-06-22 support 'when' statement, which corresponds to 'presume';
2015-06-15 wenzelm 2015-06-15 moved sections;
2015-06-15 wenzelm 2015-06-15 moved sections;
2015-06-15 wenzelm 2015-06-15 tuned;
2015-06-15 wenzelm 2015-06-15 tuned;
2015-06-13 wenzelm 2015-06-13 more on 'consider' and related concepts;
2015-06-13 wenzelm 2015-06-13 implicit rule for method "cases";
2015-06-13 wenzelm 2015-06-13 renamed "prems" to "that";
2015-06-11 wenzelm 2015-06-11 support for 'consider' command; allow full "fixes" for 'obtain' command; tuned signature;
2015-06-10 wenzelm 2015-06-10 support for "if prems" in local goal statements;
2015-06-09 wenzelm 2015-06-09 allow for_fixes for 'have', 'show' etc.; tuned signature;
2015-06-05 wenzelm 2015-06-05 added Isar command 'supply';
2015-04-18 wenzelm 2015-04-18 tuned;
2015-04-18 wenzelm 2015-04-18 clarified syntax diagram: 'obtains' does not allow prop_pat (although it could and should at some point);
2015-04-09 wenzelm 2015-04-09 make SML/NJ more happy;
2015-04-01 wenzelm 2015-04-01 misc tuning -- keep name space more clean;
2015-03-30 wenzelm 2015-03-30 more uniform syntax for named instantiations;
2015-03-23 wenzelm 2015-03-23 tuned;
2015-03-23 wenzelm 2015-03-23 clarified syntax category "fixes";
2015-03-23 wenzelm 2015-03-23 tuned syntax diagrams -- no duplication of "target";
2015-03-09 wenzelm 2015-03-09 support structural composition (THEN_ALL_NEW) for proof methods; clarified preparation for goal restriction: Goal.conjunction_tac only once; export Method.parse0, notably for Eisbach; more explicit type cases_state;
2014-10-07 wenzelm 2014-10-07 clarified whitespace;
2014-10-07 wenzelm 2014-10-07 more cartouches;
2014-10-05 wenzelm 2014-10-05 prefer @{cite} antiquotation;
2014-08-18 wenzelm 2014-08-18 merged;
2014-08-13 wenzelm 2014-08-13 tuned;
2014-08-16 wenzelm 2014-08-16 updated syntax for localized commands;