1997-11-27 wenzelm 1997-11-27 removed read_cterms;
1997-11-26 wenzelm 1997-11-26 added crep_cterm;
1997-11-24 nipkow 1997-11-24 Added read_def_cterms for simultaneous reading/typing of terms under defaults. Redefined read_def_cterm in in terms of read_def_cterms. Deleted obsolete read_cterms. Cleaned up def of read_insts, which is not much shorter but much clearere are correcter now.
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-11-20 wenzelm 1997-11-20 added transfer_sg;
1997-11-20 wenzelm 1997-11-20 tuned infer_types interface;
1997-11-06 wenzelm 1997-11-06 deriv: eliminated references to theory;
1997-11-04 wenzelm 1997-11-04 type object = exn (enhance readability);
1997-11-04 nipkow 1997-11-04 logic: loops -> rewrite_rule_ok added rewrite_rule_extra_vars thm: Rewrite rules must not introduce new type vars on rhs. This lead to an incompleteness, is now banned, and the code has been simplified.
1997-10-30 nipkow 1997-10-30 Modified trace output routines of simplifier.
1997-10-30 wenzelm 1997-10-30 tuned simp trace;
1997-10-28 wenzelm 1997-10-28 added name_of_thm; improved name_thm: does not overwrite existing name;
1997-10-24 wenzelm 1997-10-24 eq_thm (from drule.ML);
1997-10-23 wenzelm 1997-10-23 tuned;
1997-10-22 wenzelm 1997-10-22 tuned;
1997-10-21 wenzelm 1997-10-21 sg_ref: automatic adjustment of thms of draft theories;
1997-10-16 wenzelm 1997-10-16 added transfer: theory -> thm -> thm;
1997-10-16 nipkow 1997-10-16 The simplifier has been improved a little: equations s=t which used to be rejected because of looping are now treated as (s=t) == True. The latter translation must be done outside of Thm because it involves the object-logic specific True. Therefore the simple loop test has been moved from Thm to Logic.
1997-10-09 wenzelm 1997-10-09 fixed get_axiom, invoke_oracle; improved Oracle deriv;
1997-10-06 wenzelm 1997-10-06 tuned read_cterms;
1997-07-25 wenzelm 1997-07-25 added prems argument to simplification procedures;
1997-07-23 paulson 1997-07-23 Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.
1997-07-23 wenzelm 1997-07-23 improved simp tracing;
1997-07-22 wenzelm 1997-07-22 added dest_mss, merge_mss; fixed matching of simproc lhss;
1997-07-18 wenzelm 1997-07-18 tuned warning; improved comments;
1997-06-05 paulson 1997-06-05 freezeT now refers to Type.freeze_thaw
1997-04-25 wenzelm 1997-04-25 improved tmp comment;
1997-04-24 nipkow 1997-04-24 rename_params_rule used to check if the new name clashed with a free name in the whole goal state. Now checks only the subgoal concerned.
1997-04-23 wenzelm 1997-04-23 simprocs called with eta contracted subterm;
1997-04-17 wenzelm 1997-04-17 improved type check error messages;
1997-04-16 wenzelm 1997-04-16 Sorts.str_of_sort;
1997-03-14 nipkow 1997-03-14 Avoid eta-contraction in the simplifier. Instead the net needs to eta-contract the object. Also added a special function loose_bvar1(i,t) in term.ML.
1997-02-21 paulson 1997-02-21 Introduction of rotate_rule
1997-02-15 oheimb 1997-02-15 added del_congs
1997-02-14 nipkow 1997-02-14 Made troublesome simplifier warning dependent on trace_simp.
1997-01-22 nipkow 1997-01-22 Added warning msg when the simplifier cannot use a premise as a rewrite rule because it contains (type) unknowns.
1997-01-16 wenzelm 1997-01-16 added termless parameter; added simplification procedures;
1996-12-13 wenzelm 1996-12-13 fixed warning;
1996-11-28 paulson 1996-11-28 Replaced map...~~ by
1996-11-18 paulson 1996-11-18 Changed subst_bounds to subst_bound, to run faster
1996-11-13 paulson 1996-11-13 Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-12 paulson 1996-11-12 Changed some mem, ins and union calls to be monomorphic
1996-11-06 wenzelm 1996-11-06 tuned fix_shyps a little bit more;
1996-11-01 paulson 1996-11-01 Now uses Int.max instead of max nodup_Vars now updates maxidx
1996-10-30 paulson 1996-10-30 Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
1996-10-01 wenzelm 1996-10-01 added shyps comment;
1996-09-30 nipkow 1996-09-30 Inserted check for rewrite rules which introduce extra Vars on the rhs.
1996-06-28 paulson 1996-06-28 Added type-checking to rule "combination". This corrects a fault concerning soundness. See Jeremy Dawsons message of 27 Jun 1996 on isabelle-users
1996-06-14 paulson 1996-06-14 Now del_simp catches the right exception!
1996-04-30 clasohm 1996-04-30 moved dest_cimplies to drule.ML; added adjust_maxidx
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-03 nipkow 1996-04-03 Plugged some more loopholes with nodup_Vars.
1996-03-21 paulson 1996-03-21 name_thm no longer takes a theory argument, as the name no longer hides the previous derivation. Deleted sign_of_thm as redundant.
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-03-14 berghofe 1996-03-14 Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator
1996-03-11 nipkow 1996-03-11 Non-matching congruence rule in rewriter is simply ignored. Used to cause error message.
1996-03-11 paulson 1996-03-11 name_thm: now keeps the previous deriviation!
1996-03-05 paulson 1996-03-05 Addition of oracles
1996-03-01 paulson 1996-03-01 Addition of proof objects
1996-02-22 clasohm 1996-02-22 added cabs and crep_thm