| Wed, 29 Oct 2014 11:33:29 +0100 | wenzelm | modernized setup; | file | diff | annotate |
| Wed, 08 Oct 2014 17:09:07 +0200 | wenzelm | added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N}; | file | diff | annotate |
| Tue, 19 Aug 2014 12:05:11 +0200 | wenzelm | simplified type Proof.method; | file | diff | annotate |
| Thu, 20 Mar 2014 21:07:57 +0100 | wenzelm | enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range; | file | diff | annotate |
| Thu, 06 Mar 2014 13:44:01 +0100 | wenzelm | more uniform check_const/read_const; | file | diff | annotate |
| Thu, 06 Mar 2014 12:10:19 +0100 | wenzelm | tuned signature -- more uniform check_type_name/read_type_name; | file | diff | annotate |
| Sat, 14 Dec 2013 17:28:05 +0100 | wenzelm | proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; | file | diff | annotate |
| Wed, 20 Nov 2013 20:45:20 +0100 | blanchet | moved 'coinduction' proof method to 'HOL' | file | diff | annotate | base |