| Fri, 02 Feb 2001 22:19:52 +0100 | wenzelm | use hol_rewrite_cterm; | file | diff | annotate |
| Thu, 11 Jan 2001 19:38:02 +0100 | wenzelm | induct cases: RuleCases.make_raw; | file | diff | annotate |
| Sun, 07 Jan 2001 21:34:45 +0100 | wenzelm | case binds: AutoBind.drop_judgment; | file | diff | annotate |
| Sat, 06 Jan 2001 21:26:13 +0100 | wenzelm | 'of:' params spec; | file | diff | annotate |
| Fri, 22 Dec 2000 18:24:11 +0100 | wenzelm | export rewrite_cterm; | file | diff | annotate |
| Wed, 29 Nov 2000 18:42:40 +0100 | wenzelm | resolveq_cases_tac moved here from Pure/Isar/method.ML; | file | diff | annotate |
| Tue, 28 Nov 2000 01:09:40 +0100 | wenzelm | consume facts; | file | diff | annotate |
| Sun, 12 Nov 2000 14:46:16 +0100 | wenzelm | removed warning for "stripped" option; | file | diff | annotate |
| Fri, 10 Nov 2000 19:07:17 +0100 | wenzelm | inductive_rulify2 accomodates malformed induction rules; | file | diff | annotate |
| Mon, 06 Nov 2000 22:58:26 +0100 | wenzelm | method 'induct' now handles non-atomic goals; | file | diff | annotate |
| Thu, 19 Oct 2000 21:18:15 +0200 | wenzelm | split over two files: induct_attrib.ML, induct_method.ML; | file | diff | annotate |
| Sun, 17 Sep 2000 22:50:10 +0200 | wenzelm | made SML/NJ happy; | file | diff | annotate |
| Sun, 17 Sep 2000 22:21:31 +0200 | wenzelm | Display.pretty_thm_sg; | file | diff | annotate |
| Mon, 11 Sep 2000 17:35:17 +0200 | wenzelm | case args: align_right; | file | diff | annotate |
| Thu, 07 Sep 2000 20:51:07 +0200 | wenzelm | tuned msg; | file | diff | annotate |
| Sat, 02 Sep 2000 21:49:51 +0200 | wenzelm | use Args.mode; | file | diff | annotate |
| Thu, 17 Aug 2000 10:37:04 +0200 | wenzelm | changed 'opaque' option to 'open' (opaque is default); | file | diff | annotate |
| Mon, 14 Aug 2000 18:13:42 +0200 | wenzelm | cases: support multiple insts; | file | diff | annotate |
| Thu, 13 Jul 2000 23:11:14 +0200 | wenzelm | fixed simplified_cases; | file | diff | annotate |
| Thu, 13 Jul 2000 11:44:02 +0200 | wenzelm | added simp_case_tac; | file | diff | annotate |
| Sat, 01 Jul 2000 19:55:22 +0200 | wenzelm | GPLed; | file | diff | annotate |
| Wed, 14 Jun 2000 17:59:53 +0200 | wenzelm | theorems [cases type: bool] = case_split; | file | diff | annotate |
| Fri, 05 May 2000 22:32:25 +0200 | wenzelm | use Args.colon / Args.parens; | file | diff | annotate |
| Wed, 12 Apr 2000 23:51:57 +0200 | wenzelm | export concl_of; | file | diff | annotate |
| Wed, 12 Apr 2000 18:53:09 +0200 | wenzelm | induct stripped: match_tac; | file | diff | annotate |
| Wed, 05 Apr 2000 21:02:31 +0200 | wenzelm | HEADGOAL; | file | diff | annotate |
| Mon, 20 Mar 2000 18:48:43 +0100 | wenzelm | tuned degenerate cases / induct; | file | diff | annotate |
| Tue, 14 Mar 2000 11:33:30 +0100 | wenzelm | tuned comments; | file | diff | annotate |
| Mon, 13 Mar 2000 13:19:14 +0100 | wenzelm | export vars_of; | file | diff | annotate |
| Thu, 09 Mar 2000 22:56:40 +0100 | wenzelm | cleaned comment; | file | diff | annotate |