1998-12-04 paulson 1998-12-04 better export for nested locales
1998-11-25 wenzelm 1998-11-25 removed redirect_to_latex stuff;
1998-10-29 wenzelm 1998-10-29 tuned current_goals_markers semantics to avoid empty lines;
1998-10-23 paulson 1998-10-23 better reporting of "Additional hypotheses" in a locale
1998-10-22 wenzelm 1998-10-22 support current_goals_markers ref variable for print_current_goals;
1998-10-05 paulson 1998-10-05 Now prove_goalw_cterm never prints timing statistics
1998-08-13 paulson 1998-08-13 Rule mk_triv_goal for making instances of triv_goal
1998-08-04 wenzelm 1998-08-04 added export: thm -> thm; exported print_current_goals_default; locale support;
1998-06-29 wenzelm 1998-06-29 moved actual (C)Pure theories to pure.ML;
1998-06-17 nipkow 1998-06-17 Goals may now contain assumptions, which are not returned. This is controlled by an argument `atomic' to the goal commands.
1998-06-05 wenzelm 1998-06-05 tuned print_exn;
1997-11-22 wenzelm 1997-11-22 fixed warning;
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-11-12 wenzelm 1997-11-12 moved 'latex' from library.ML to goals.ML;
1997-10-24 wenzelm 1997-10-24 Pure.thy;
1997-10-23 wenzelm 1997-10-23 Sign.stamp_names_of;
1997-10-13 wenzelm 1997-10-13 uses Sign.str_of_sort;
1997-09-25 paulson 1997-09-25 Prints warnings using the "warning" function instead of "writeln"
1997-09-11 wenzelm 1997-09-11 removed print_goals_ref (which was broken anyway);
1997-07-18 wenzelm 1997-07-18 tuned error propagation msg;
1997-07-18 wenzelm 1997-07-18 tuned warnings; print_current_goals_fn, result_error_fn hooks replace print_goals_ref;
1997-04-16 wenzelm 1997-04-16 Sorts.str_of_sort;
1997-04-02 wenzelm 1997-04-02 changed signature of dummy goal from proto_pure to pure;
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