src/Pure/logic.ML
2006-10-07 wenzelm 2006-10-07 removed is_equals, is_implies; tuned;
2006-09-19 wenzelm 2006-09-19 added name_classrel/arities/arity;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.invent_list;
2006-06-13 wenzelm 2006-06-13 (un)varify: tuned exceptions;
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-06-05 wenzelm 2006-06-05 support embedded terms;
2006-04-13 wenzelm 2006-04-13 added dest_conjunction_list; close_form: canonical order of variables;
2006-04-11 wenzelm 2006-04-11 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML); tuned;
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-02-22 wenzelm 2006-02-22 simplified Pure conjunction, based on actual const;
2006-02-18 wenzelm 2006-02-18 dest_def: tuned error msg;
2006-02-16 wenzelm 2006-02-16 dest_def: actually return beta-eta contracted equation;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 added generic dest_def (mostly from theory.ML); added abs_def (from Isar/local_defs.ML); added const_of_class/class_of_const (from sign.ML); added combound, rlist_abs (from unify.ML);
2006-01-24 wenzelm 2006-01-24 added dest_all;
2005-12-23 wenzelm 2005-12-23 added mk_conjunction_list2;
2005-12-22 wenzelm 2005-12-22 mk_conjunction: proper treatment of bounds; added dest_conjunction(s);
2005-11-25 wenzelm 2005-11-25 tuned;
2005-11-16 wenzelm 2005-11-16 tuned;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces; replaced lift_fns by lift_abs, lift_all;
2005-08-18 paulson 2005-08-18 optimization to incr_indexes?
2005-07-19 wenzelm 2005-07-19 incr_tvar (from term.ML), incr_indexes: avoid garbage;
2005-07-15 wenzelm 2005-07-15 tuned;
2005-07-14 wenzelm 2005-07-14 occs no longer infix (structure not open);
2005-05-31 wenzelm 2005-05-31 added nth_prem;
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-01-24 paulson 2005-01-24 thin_tac now works on P==>Q
2005-01-21 paulson 2005-01-21 fixed thin_tac with higher-level assumptions by removing the old code to handle the iterated introduction of parameters
2003-07-31 berghofe 2003-07-31 Removed extraneous rev in function goal_params (the list of parameters is already reversed by rename_wrt_term).
2003-07-11 berghofe 2003-07-11 Exported function goal_params.
2003-02-03 berghofe 2003-02-03 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
2002-10-21 berghofe 2002-10-21 Removed obsolete functions dealing with flex-flex constraints.
2002-02-20 wenzelm 2002-02-20 Symbol.bump_string;
2002-01-17 wenzelm 2002-01-17 is_norm_hhf moved to drule.ML;
2002-01-15 wenzelm 2002-01-15 added mk_conjunction_list;
2001-11-11 wenzelm 2001-11-11 added mk_conjunction;
2001-01-07 wenzelm 2001-01-07 added is_norm_hhf;
2000-11-10 wenzelm 2000-11-10 has_meta_prems: include "==";
2000-08-24 paulson 2000-08-24 fixed strip_assums and assum_pairs, restoring them (essentially) to their 1989 versions. They had been "optimized" for flattened parameters, but failed when given an initial, non-flattened proof state. A manifestation of the bug is Goal "of the bug isf. EX B. Q(f,B) ==> (of the bug isy. P(f,y))"; be exE 1;
2000-08-21 wenzelm 2000-08-21 fixed has_meta_prems: strip_assums_hyp;
2000-08-01 wenzelm 2000-08-01 added has_meta_prems;
2000-07-30 wenzelm 2000-07-30 Logic.goal_const;
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-04-22 wenzelm 1998-04-22 added mk_cond_defpair, mk_defpair;
1998-03-09 wenzelm 1998-03-09 adapted to baroque chars;
1998-03-04 nipkow 1998-03-04 Reorganized simplifier. May now reorient rules. Moved loop tests from logic to thm.
1998-02-28 nipkow 1998-02-28 Tried to reorganize rewriter a little. More to be done.
1998-02-18 nipkow 1998-02-18 Improved loop-test for rewrite rules a little. Should be done properly!
1997-12-19 wenzelm 1997-12-19 term order stuff moved to term.ML;
1997-12-02 wenzelm 1997-12-02 tuned term order; added indexname_ord, typ_ord, typs_ord, term_ord, terms_ord;
1997-11-28 nipkow 1997-11-28 Fixed the definition of `termord': is now antisymmetric.
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-21 nipkow 1997-10-21 Corrected alphabetical order of entries in signature.
1997-10-17 paulson 1997-10-17 Added "op" before "occs" to make sml/nj happy
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-06-05 paulson 1997-06-05 Removal of freeze_vars and thaw_vars (quite unused...)
1997-01-16 wenzelm 1997-01-16 added term order;
1996-11-28 paulson 1996-11-28 Replaced map...~~ by ListPair.map
1996-06-28 paulson 1996-06-28 Restored warning comment