| Fri, 14 Dec 2001 11:50:38 +0100 | wenzelm | changed Type.varify; | file | diff | annotate |
| Thu, 06 Dec 2001 00:40:56 +0100 | wenzelm | added the_mk_cases; | file | diff | annotate |
| Sat, 01 Dec 2001 18:52:32 +0100 | wenzelm | renamed class "term" to "type" (actually "HOL.type"); | file | diff | annotate |
| Wed, 28 Nov 2001 00:46:26 +0100 | wenzelm | theory data: removed obsolete finish method; | file | diff | annotate |
| Wed, 21 Nov 2001 00:34:06 +0100 | wenzelm | Set.vimage; | file | diff | annotate |
| Wed, 14 Nov 2001 18:44:27 +0100 | wenzelm | inductive: removed con_defs; | file | diff | annotate |
| Tue, 13 Nov 2001 22:18:46 +0100 | wenzelm | tuned; | file | diff | annotate |
| Mon, 12 Nov 2001 23:27:04 +0100 | wenzelm | mutual rules declared as ``consumes 0''; | file | diff | annotate |
| Fri, 09 Nov 2001 22:50:58 +0100 | wenzelm | tuned; | file | diff | annotate |
| Thu, 08 Nov 2001 23:59:37 +0100 | wenzelm | theory data: finish method; | file | diff | annotate |
| Wed, 31 Oct 2001 01:21:31 +0100 | wenzelm | use HOL.induct_XXX; | file | diff | annotate |
| Mon, 22 Oct 2001 17:58:26 +0200 | wenzelm | quick_and_dirty_prove_goalw_cterm; | file | diff | annotate |
| Thu, 18 Oct 2001 21:27:47 +0200 | wenzelm | GPLed; | file | diff | annotate |
| Thu, 18 Oct 2001 21:05:35 +0200 | wenzelm | moved atomize stuff to theory HOL; | file | diff | annotate |
| Mon, 15 Oct 2001 20:35:10 +0200 | wenzelm | Tactic.rewrite_cterm; | file | diff | annotate |
| Sun, 14 Oct 2001 22:08:29 +0200 | wenzelm | moved rulify to ObjectLogic; | file | diff | annotate |
| Sun, 14 Oct 2001 20:05:07 +0200 | wenzelm | "HOL.mono"; | file | diff | annotate |
| Sat, 13 Oct 2001 20:31:34 +0200 | wenzelm | IsarThy.theorem_i Drule.internalK; | file | diff | annotate |
| Thu, 04 Oct 2001 15:39:43 +0200 | wenzelm | simp_case_tac is back again from induct_method.ML; | file | diff | annotate |
| Fri, 28 Sep 2001 19:19:26 +0200 | wenzelm | inductive: no collective atts; | file | diff | annotate |
| Thu, 16 Aug 2001 23:19:12 +0200 | wenzelm | prefer immediate monos; | file | diff | annotate |
| Fri, 01 Jun 2001 11:03:50 +0200 | paulson | now checks for leading meta-quantifiers and complains, instead of | file | diff | annotate |
| Fri, 02 Feb 2001 22:20:09 +0100 | wenzelm | use hol_simplify; | file | diff | annotate |
| Wed, 31 Jan 2001 01:13:01 +0100 | wenzelm | more robust handling of rule cases hints; | file | diff | annotate |
| Mon, 29 Jan 2001 13:26:04 +0100 | berghofe | Splitting of arguments of product types in induction rules is now less | file | diff | annotate |
| Tue, 16 Jan 2001 00:32:38 +0100 | wenzelm | export inductive_forall_name, inductive_forall_def, rulify; | file | diff | annotate |
| Sat, 06 Jan 2001 21:26:27 +0100 | wenzelm | Tactic.norm_hhf; | file | diff | annotate |
| Wed, 27 Dec 2000 18:27:19 +0100 | wenzelm | Method.erule 0; | file | diff | annotate |
| Sat, 23 Dec 2000 22:51:34 +0100 | wenzelm | simplified quick_and_dirty stuff; | file | diff | annotate |
| Fri, 22 Dec 2000 18:24:39 +0100 | wenzelm | handle proper rules; | file | diff | annotate |