| 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 |