| Tue, 01 Jun 2004 12:33:50 +0200 | wenzelm | removed obsolete sort 'logic'; | file | diff | annotate |
| Sat, 29 May 2004 15:00:52 +0200 | wenzelm | improved output; | file | diff | annotate |
| Fri, 21 May 2004 21:23:12 +0200 | wenzelm | test_classrel/arity improve error reporting; tuned; | file | diff | annotate |
| Sat, 01 May 2004 22:08:57 +0200 | wenzelm | improved Term.invent_names; | file | diff | annotate |
| Fri, 16 Apr 2004 20:59:09 +0200 | wenzelm | 'instance' and intro_classes now handle general sorts; | file | diff | annotate |
| Tue, 12 Feb 2002 20:28:27 +0100 | wenzelm | got rid of explicit marginal comments (now stripped earlier from input); | file | diff | annotate |
| Thu, 10 Jan 2002 01:11:43 +0100 | wenzelm | simplified IsarThy.theorem_i; | file | diff | annotate |
| Fri, 14 Dec 2001 11:50:19 +0100 | wenzelm | Term.invent_type_names; | file | diff | annotate |
| Wed, 05 Dec 2001 03:06:05 +0100 | wenzelm | tuned; | file | diff | annotate |
| Wed, 28 Nov 2001 00:46:26 +0100 | wenzelm | theory data: removed obsolete finish method; | file | diff | annotate |
| Fri, 09 Nov 2001 00:19:20 +0100 | wenzelm | theory data: finish method; | file | diff | annotate |
| Sun, 04 Nov 2001 20:56:59 +0100 | wenzelm | IsarThy.theorem_i (None, []); | file | diff | annotate |
| Wed, 31 Oct 2001 21:59:07 +0100 | wenzelm | IsarThy.theorem_i: no locale; | file | diff | annotate |
| Sat, 27 Oct 2001 23:18:40 +0200 | wenzelm | removed obsolete goal_subclass, goal_arity; | file | diff | annotate |
| Thu, 18 Oct 2001 21:02:26 +0200 | wenzelm | sane internal interfaces for instance; | file | diff | annotate |
| Sat, 13 Oct 2001 20:31:34 +0200 | wenzelm | IsarThy.theorem_i Drule.internalK; | file | diff | annotate |
| Fri, 31 Aug 2001 22:45:08 +0200 | wenzelm | proper use of invent_names; | file | diff | annotate |
| Fri, 31 Aug 2001 18:46:48 +0200 | wenzelm | tuned headers; | file | diff | annotate |
| Thu, 31 May 2001 17:57:02 +0200 | wenzelm | invent_names | file | diff | annotate |
| Mon, 12 Feb 2001 20:45:12 +0100 | wenzelm | support \<subseteq> syntax in classes/classrel/axclass/instance; | file | diff | annotate |
| Tue, 21 Nov 2000 19:04:03 +0100 | wenzelm | Tactic.distinct_subgoals_tac moved to internal intro_classes_tac; | file | diff | annotate |
| Sat, 18 Nov 2000 19:47:36 +0100 | wenzelm | default_intro_classes_tac: Tactic.distinct_subgoals_tac; | file | diff | annotate |
| Mon, 13 Nov 2000 21:59:49 +0100 | wenzelm | tuned IsarThy.theorem_i; | file | diff | annotate |
| Mon, 23 Oct 2000 22:10:36 +0200 | wenzelm | intro_classes by default; | file | diff | annotate |
| Sun, 17 Sep 2000 22:21:31 +0200 | wenzelm | Display.pretty_thm_sg; | file | diff | annotate |
| Tue, 23 May 2000 12:30:29 +0200 | paulson | eta-expanded to handle value polymorphism | file | diff | annotate |
| Sun, 21 May 2000 14:35:27 +0200 | wenzelm | adapted to inner syntax of sorts; | file | diff | annotate |
| Mon, 17 Apr 2000 13:57:55 +0200 | wenzelm | Pretty.chunks; | file | diff | annotate |
| Fri, 14 Apr 2000 17:30:22 +0200 | wenzelm | intrn_arity: reject type abbreviations; | file | diff | annotate |
| Wed, 05 Apr 2000 21:02:31 +0200 | wenzelm | HEADGOAL; | file | diff | annotate |
| Sat, 18 Mar 2000 19:19:53 +0100 | wenzelm | intro_classes_tac: REPEAT_ALL_NEW; | file | diff | annotate |
| Mon, 13 Mar 2000 12:25:52 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | file | diff | annotate |
| Wed, 25 Aug 1999 20:38:56 +0200 | wenzelm | expand_classes renamed to intro_classes; | file | diff | annotate |
| Thu, 08 Jul 1999 18:36:09 +0200 | wenzelm | propp: 'concl' patterns; | file | diff | annotate |
| Tue, 25 May 1999 20:24:10 +0200 | wenzelm | formal comments (still dummy); | file | diff | annotate |
| Mon, 24 May 1999 21:53:18 +0200 | wenzelm | outer syntax keyword classification; | file | diff | annotate |
| Fri, 21 May 1999 11:36:02 +0200 | wenzelm | improved errors; | file | diff | annotate |
| Fri, 30 Apr 1999 18:01:11 +0200 | wenzelm | theory data: copy; | file | diff | annotate |
| Wed, 17 Mar 1999 16:33:00 +0100 | wenzelm | qualify Theory.sign_of etc.; | file | diff | annotate |
| Wed, 17 Mar 1999 13:44:43 +0100 | wenzelm | theory data; | file | diff | annotate |
| Tue, 12 Jan 1999 12:29:24 +0100 | wenzelm | eliminated Attribute structure; | file | diff | annotate |
| Tue, 20 Oct 1998 16:25:54 +0200 | wenzelm | quiet_mode, message; | file | diff | annotate |
| Fri, 15 May 1998 11:35:56 +0200 | wenzelm | witnesses: lookup stored thms instead of axioms; | file | diff | annotate |
| Wed, 13 May 1998 12:17:49 +0200 | wenzelm | tuned msg; | file | diff | annotate |
| Wed, 29 Apr 1998 11:14:34 +0200 | wenzelm | adapted to new PureThy.add_axioms_i; | file | diff | annotate |
| Tue, 28 Oct 1997 17:27:10 +0100 | wenzelm | add_store_axioms_i; | file | diff | annotate |
| Fri, 24 Oct 1997 17:11:48 +0200 | wenzelm | removed add_thms_as_axms; | file | diff | annotate |
| Mon, 20 Oct 1997 15:20:20 +0200 | wenzelm | tuned types; | file | diff | annotate |
| Mon, 20 Oct 1997 11:47:04 +0200 | wenzelm | fixed goal_XXX; | file | diff | annotate |
| Mon, 20 Oct 1997 10:52:32 +0200 | wenzelm | fixed types of add_XXX; | file | diff | annotate |
| Mon, 13 Oct 1997 17:49:08 +0200 | wenzelm | uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity; | file | diff | annotate |
| Thu, 09 Oct 1997 14:39:44 +0200 | wenzelm | fixed axiom names; | file | diff | annotate |
| Mon, 06 Oct 1997 18:57:17 +0200 | wenzelm | eliminated raise_term, raise_typ; | file | diff | annotate |
| Wed, 01 Oct 1997 17:40:09 +0200 | wenzelm | fully qualified names: Theory.add_XXX; | file | diff | annotate |
| Wed, 06 Aug 1997 15:07:33 +0200 | wenzelm | added "Proving ..." msgs; | file | diff | annotate |
| Wed, 04 Jun 1997 12:26:42 +0200 | wenzelm | eliminated freeze_vars; | file | diff | annotate |
| Wed, 16 Apr 1997 18:21:00 +0200 | wenzelm | Sorts.str_of_arity; | file | diff | annotate |
| Fri, 21 Feb 1997 15:31:47 +0100 | paulson | Replaced "flat" by the Basis Library function List.concat | file | diff | annotate |
| Thu, 28 Nov 1996 10:44:24 +0100 | paulson | Replaced map...~~ by ListPair.map | file | diff | annotate |
| Fri, 16 Feb 1996 11:35:52 +0100 | paulson | Elimination of fully-functorial style. | file | diff | annotate |