doc-src/Ref/thm.tex
Fri, 28 Sep 2001 18:55:37 +0200 berghofe Tuned section about parsing and printing proof terms.
Fri, 28 Sep 2001 16:44:27 +0200 berghofe Added documentation for proof terms.
Tue, 20 Feb 2001 18:47:22 +0100 oheimb added rearrange_prems
Wed, 02 Aug 2000 19:37:36 +0200 wenzelm rep_thm: 'der' field has additional bool for oracles;
Wed, 12 Jul 2000 16:44:34 +0200 wenzelm infix 'OF' is a version of 'MRS' with more appropriate argument order;
Thu, 06 Jul 2000 11:23:39 +0200 paulson fixed typos reported by Jeremy Dawson
Thu, 25 May 2000 15:12:00 +0200 paulson documented permute_prems
Tue, 18 Jan 2000 11:33:31 +0100 paulson fixed many bad line & page breaks
Tue, 18 Jan 2000 11:00:10 +0100 paulson Documented Thm.instantiate (not normalizing) and Drule.instantiate
Fri, 15 Oct 1999 12:31:43 +0200 berghofe Documented thm_deps.
Wed, 29 Sep 1999 14:34:01 +0200 wenzelm strip_shyps(_warning);
Thu, 08 Jul 1999 18:27:01 +0200 wenzelm Theorems involving oracles will be printed with a suffixed \verb|[!]|;
Tue, 12 Jan 1999 15:39:34 +0100 wenzelm fixed deriv;
Thu, 29 Oct 1998 15:06:10 +0100 wenzelm shyps note for prim. rules;
Mon, 24 Aug 1998 19:12:13 +0200 wenzelm emacs local vars;
Sat, 07 Feb 1998 14:37:48 +0100 paulson Added reference to rotate_prems
Thu, 05 Feb 1998 10:26:59 +0100 paulson Fixed a lot of overfull and underfull lines (hboxes)
Mon, 08 Dec 1997 13:57:19 +0100 paulson Tidying to fix overfull lines, etc
Fri, 05 Dec 1997 18:46:18 +0100 wenzelm instantiate';
Thu, 27 Nov 1997 19:39:02 +0100 wenzelm several minor updates;
Fri, 21 Nov 1997 15:41:27 +0100 wenzelm changed Pure/Sequence interface;
Thu, 04 Sep 1997 17:43:16 +0200 paulson Deleted an obsolete description of rewrite_cterm. The current version uses
Thu, 17 Jul 1997 15:03:38 +0200 wenzelm fixed EqI meta rule;
Wed, 02 Jul 1997 16:46:36 +0200 paulson Now there are TWO spaces after each full stop, so that the Emacs sentence
Wed, 07 May 1997 17:21:24 +0200 wenzelm tuned spaces;
Tue, 06 May 1997 12:50:16 +0200 wenzelm misc updates, tuning, cleanup;
Mon, 30 Sep 1996 11:04:14 +0200 paulson Improved discussion of shyps thanks to Markus Wenzel
Thu, 26 Sep 1996 17:15:19 +0200 paulson Documented sort hypotheses and improved discussion of derivations
Mon, 22 Jul 1996 16:15:00 +0200 paulson Corrected typo involving derivations
Thu, 11 Jul 1996 15:00:38 +0200 paulson Documentation of oracles and their syntax
Wed, 20 Mar 1996 18:36:59 +0100 paulson Describes proof objects and Deriv module
Thu, 11 May 1995 10:42:19 +0200 lcp Indexing of COMP
Tue, 24 Jan 1995 03:04:20 +0100 lcp Under RS added cross reference to bind_thm
Thu, 19 Jan 1995 16:05:21 +0100 clasohm added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
Fri, 22 Apr 1994 18:18:37 +0200 lcp final Springer copy
Fri, 15 Apr 1994 18:04:01 +0200 lcp penultimate Springer draft
Mon, 21 Mar 1994 11:02:57 +0100 lcp first draft of Springer book
Thu, 25 Nov 1993 14:42:46 +0100 wenzelm corrected some obvious errors;
Wed, 10 Nov 1993 05:00:57 +0100 lcp Initial revision
less more (0) tip