src/Pure/logic.ML
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
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
1994-10-12 wenzelm 1994-10-12 added is_equals: term -> bool;
1994-09-06 lcp 1994-09-06 Pure/type/unvarifyT: moved there from logic.ML
1994-08-18 lcp 1994-08-18 /unvarifyT, unvarify: moved to Pure/logic.ML
1994-07-06 wenzelm 1994-07-06 changed comment only;
1994-05-26 wenzelm 1994-05-26 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses); restored functor sig constraint :LOGIC;
1994-01-04 wenzelm 1994-01-04 commented out sig constraint of functor (for debugging purposes);
1993-10-21 lcp 1993-10-21 logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of. So it no longer checks t properly -- but it never checked u anyway, and all existing calls are derived from certified terms...
1993-09-16 clasohm 1993-09-16 Initial revision