src/Pure/goals.ML
1997-02-04 paulson 1997-02-04 Gradual switching to Basis Library functions nth, drop, etc.
1997-01-17 paulson 1997-01-17 Added the prlim command
1996-11-08 paulson 1996-11-08 Removed "standard" call from uresult, to allow specialist applications
1996-10-24 paulson 1996-10-24 Allowing negative levels (as offsets) in prlev and choplev
1996-08-20 paulson 1996-08-20 Added ref to allow suppression of error msgs
1996-03-28 berghofe 1996-03-28 Added functions pr_latex and printgoal_latex which display current proof state in xdvi window
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-03-11 paulson 1996-03-11 Made an exception handler more specific
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1995-12-22 paulson 1995-12-22 "prepare_proof" has been simplified because rewrite_rule and rewrite_goals_rule check for empty lists. The list of premises is *not* passed to Thm.compress; this was tried, but the potential storage gains seemed not to justify the cpu time required.
1995-09-01 wenzelm 1995-09-01 adapted to new version of shyps-stuff;
1995-08-01 wenzelm 1995-08-01 modified prepare_proof to handle shyps;
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-02-27 lcp 1995-02-27 Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest of the error message ("The exception above was raised for...") will appear. And print_exn calls print_sign_exn_unit so that it can re-raise the SAME exception.
1994-11-03 lcp 1994-11-03 Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final result.
1994-11-02 nipkow 1994-11-02 Modified pattern.ML to perform proper matching of Higher-Order Patterns. Modified thm.ML to preserve bound var names during rewriting. Renamed eta_matches to matches.
1994-08-25 lcp 1994-08-25 print_sign_exn: now exported, with a polymorphic type
1994-08-18 lcp 1994-08-18 Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved from prove_goalw
1994-02-03 wenzelm 1994-02-03 replaced eq_sg by Sign.eq_sg;
1994-01-18 lcp 1994-01-18 Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g
1993-10-22 lcp 1993-10-22 goals/print_top,prepare_proof: now call \!print_goals_ref
1993-10-08 wenzelm 1993-10-08 "The error/exception above ...": errorneous goal now quoted;
1993-09-16 clasohm 1993-09-16 Initial revision