src/Pure/thm.ML
Fri, 06 Mar 1998 16:05:04 +0100 nipkow Removed superfluous `op'
Wed, 04 Mar 1998 13:16:05 +0100 nipkow Reorganized simplifier. May now reorient rules.
Sat, 28 Feb 1998 15:40:03 +0100 nipkow Tried to reorganize rewriter a little. More to be done.
Fri, 30 Jan 1998 11:33:01 +0100 wenzelm improved tracing of rewrite rule application;
Fri, 19 Dec 1997 09:58:42 +0100 wenzelm Term.termless;
Fri, 12 Dec 1997 17:14:58 +0100 wenzelm tuned msg;
Thu, 27 Nov 1997 19:36:51 +0100 wenzelm removed read_cterms;
Wed, 26 Nov 1997 16:38:04 +0100 wenzelm added crep_cterm;
Mon, 24 Nov 1997 16:43:43 +0100 nipkow Added read_def_cterms for simultaneous reading/typing of terms under
Fri, 21 Nov 1997 15:27:43 +0100 wenzelm changed Sequence interface (now Seq, in seq.ML);
Thu, 20 Nov 1997 15:06:57 +0100 wenzelm added transfer_sg;
Thu, 20 Nov 1997 12:51:55 +0100 wenzelm tuned infer_types interface;
Thu, 06 Nov 1997 16:41:08 +0100 wenzelm deriv: eliminated references to theory;
Tue, 04 Nov 1997 16:17:04 +0100 wenzelm type object = exn (enhance readability);
Tue, 04 Nov 1997 12:58:10 +0100 nipkow logic: loops -> rewrite_rule_ok
Thu, 30 Oct 1997 16:57:09 +0100 nipkow Modified trace output routines of simplifier.
Thu, 30 Oct 1997 09:59:38 +0100 wenzelm tuned simp trace;
Tue, 28 Oct 1997 17:30:47 +0100 wenzelm added name_of_thm;
Fri, 24 Oct 1997 17:15:59 +0200 wenzelm eq_thm (from drule.ML);
Thu, 23 Oct 1997 12:09:31 +0200 wenzelm tuned;
Wed, 22 Oct 1997 11:36:43 +0200 wenzelm tuned;
Tue, 21 Oct 1997 18:09:13 +0200 wenzelm sg_ref: automatic adjustment of thms of draft theories;
Thu, 16 Oct 1997 14:00:20 +0200 wenzelm added transfer: theory -> thm -> thm;
Thu, 16 Oct 1997 13:45:16 +0200 nipkow The simplifier has been improved a little: equations s=t which used to be
Thu, 09 Oct 1997 14:52:36 +0200 wenzelm fixed get_axiom, invoke_oracle;
Mon, 06 Oct 1997 18:59:49 +0200 wenzelm tuned read_cterms;
Fri, 25 Jul 1997 13:18:09 +0200 wenzelm added prems argument to simplification procedures;
Wed, 23 Jul 1997 11:54:32 +0200 paulson Now rename_params_rule merely issues warnings--and does nothing--if the
Wed, 23 Jul 1997 11:04:19 +0200 wenzelm improved simp tracing;
Tue, 22 Jul 1997 18:45:43 +0200 wenzelm added dest_mss, merge_mss;
Fri, 18 Jul 1997 13:36:43 +0200 wenzelm tuned warning;
Thu, 05 Jun 1997 13:53:59 +0200 paulson freezeT now refers to Type.freeze_thaw
Fri, 25 Apr 1997 17:50:55 +0200 wenzelm improved tmp comment;
Thu, 24 Apr 1997 17:59:55 +0200 nipkow rename_params_rule used to check if the new name clashed with a free name in
Wed, 23 Apr 1997 10:08:51 +0200 wenzelm simprocs called with eta contracted subterm;
Thu, 17 Apr 1997 18:46:58 +0200 wenzelm improved type check error messages;
Wed, 16 Apr 1997 18:22:10 +0200 wenzelm Sorts.str_of_sort;
Fri, 14 Mar 1997 10:35:30 +0100 nipkow Avoid eta-contraction in the simplifier.
Fri, 21 Feb 1997 15:30:41 +0100 paulson Introduction of rotate_rule
Sat, 15 Feb 1997 16:04:33 +0100 oheimb added del_congs
Fri, 14 Feb 1997 12:19:42 +0100 nipkow Made troublesome simplifier warning dependent on trace_simp.
Wed, 22 Jan 1997 18:17:36 +0100 nipkow Added warning msg when the simplifier cannot use a premise as a rewrite rule
Thu, 16 Jan 1997 14:53:37 +0100 wenzelm added termless parameter;
Fri, 13 Dec 1996 17:38:17 +0100 wenzelm fixed warning;
Thu, 28 Nov 1996 10:44:24 +0100 paulson Replaced map...~~ by ListPair.map
Mon, 18 Nov 1996 16:30:06 +0100 paulson Changed subst_bounds to subst_bound, to run faster
Wed, 13 Nov 1996 10:42:50 +0100 paulson Removal of polymorphic equality via mem, subset, eq_set, etc
Tue, 12 Nov 1996 11:43:16 +0100 paulson Changed some mem, ins and union calls to be monomorphic
Wed, 06 Nov 1996 12:49:31 +0100 wenzelm tuned fix_shyps a little bit more;
Fri, 01 Nov 1996 15:35:28 +0100 paulson Now uses Int.max instead of max
Wed, 30 Oct 1996 11:20:27 +0100 paulson Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
Tue, 01 Oct 1996 10:43:58 +0200 wenzelm added shyps comment;
Mon, 30 Sep 1996 15:29:52 +0200 nipkow Inserted check for rewrite rules which introduce extra Vars on the rhs.
Fri, 28 Jun 1996 11:13:07 +0200 paulson Added type-checking to rule "combination". This corrects a fault
Fri, 14 Jun 1996 12:27:48 +0200 paulson Now del_simp catches the right exception!
Tue, 30 Apr 1996 12:03:01 +0200 clasohm moved dest_cimplies to drule.ML; added adjust_maxidx
Wed, 17 Apr 1996 11:46:10 +0200 oheimb *** empty log message ***
Wed, 03 Apr 1996 14:06:34 +0200 nipkow Plugged some more loopholes with nodup_Vars.
Thu, 21 Mar 1996 11:06:59 +0100 paulson name_thm no longer takes a theory argument, as the
Fri, 15 Mar 1996 12:01:19 +0100 berghofe Added some functions which allow redirection of Isabelle's output
less more (0) -100 -60 tip