src/Pure/goals.ML
Thu, 24 Oct 1996 10:42:42 +0200 paulson Allowing negative levels (as offsets) in prlev and choplev
Tue, 20 Aug 1996 12:40:17 +0200 paulson Added ref to allow suppression of error msgs
Thu, 28 Mar 1996 17:27:54 +0100 berghofe Added functions pr_latex and printgoal_latex which
Fri, 15 Mar 1996 12:01:19 +0100 berghofe Added some functions which allow redirection of Isabelle's output
Mon, 11 Mar 1996 14:13:36 +0100 paulson Made an exception handler more specific
Fri, 16 Feb 1996 12:19:47 +0100 paulson Elimination of fully-functorial style.
Mon, 29 Jan 1996 14:16:13 +0100 clasohm inserted tabs again
Mon, 29 Jan 1996 13:56:41 +0100 clasohm removed tabs
Fri, 22 Dec 1995 10:26:57 +0100 paulson "prepare_proof" has been simplified because
Fri, 01 Sep 1995 13:16:24 +0200 wenzelm adapted to new version of shyps-stuff;
Tue, 01 Aug 1995 17:21:05 +0200 wenzelm modified prepare_proof to handle shyps;
Fri, 03 Mar 1995 11:48:05 +0100 clasohm added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
Mon, 27 Feb 1995 18:07:59 +0100 lcp Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
Thu, 03 Nov 1994 16:52:19 +0100 lcp Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
Wed, 02 Nov 1994 09:09:30 +0100 nipkow Modified pattern.ML to perform proper matching of Higher-Order Patterns.
Thu, 25 Aug 1994 10:41:17 +0200 lcp print_sign_exn: now exported, with a polymorphic type
Thu, 18 Aug 1994 17:53:28 +0200 lcp Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
Thu, 03 Feb 1994 13:55:20 +0100 wenzelm replaced eq_sg by Sign.eq_sg;
Tue, 18 Jan 1994 15:57:40 +0100 lcp Many other files modified as follows:
Fri, 22 Oct 1993 10:31:19 +0100 lcp goals/print_top,prepare_proof: now call \!print_goals_ref
Fri, 08 Oct 1993 12:30:01 +0100 wenzelm "The error/exception above ...": errorneous goal now quoted;
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip