src/Pure/drule.ML
Thu, 17 Oct 2002 10:52:59 +0200 paulson fixing the cut_tac method to work when there are no instantiations and the
Mon, 30 Sep 2002 16:37:44 +0200 berghofe Removed nRS again because extract_rews now takes care of preserving names.
Thu, 19 Sep 2002 16:01:29 +0200 nipkow drule: added nRS
Thu, 18 Jul 2002 12:05:51 +0200 wenzelm added satisfy_hyps;
Tue, 16 Jul 2002 18:37:03 +0200 wenzelm added equal_elim_rule1;
Tue, 09 Jul 2002 18:03:26 +0200 berghofe Added function abs_def.
Fri, 31 May 2002 18:50:03 +0200 berghofe Changed interface of Pattern.rewrite_term.
Tue, 07 May 2002 14:26:32 +0200 wenzelm use eq_thm_prop instead of slightly inadequate eq_thm;
Wed, 20 Feb 2002 16:00:32 +0100 berghofe New function strip_comb (cterm version of Term.strip_comb).
Thu, 17 Jan 2002 21:02:52 +0100 wenzelm added is_norm_hhf (from logic.ML);
Tue, 15 Jan 2002 00:09:29 +0100 wenzelm conj_intr_list and conj_elim_precise: cover 0 conjuncts;
Sat, 12 Jan 2002 16:37:58 +0100 wenzelm renamed forall_elim_vars_safe to gen_all;
Fri, 11 Jan 2002 14:53:05 +0100 wenzelm improved forall_elim_vars_safe (no longer invents new indexes);
Fri, 11 Jan 2002 00:29:25 +0100 wenzelm kind: ignore "";
Tue, 18 Dec 2001 02:17:20 +0100 wenzelm tuned Type.unify;
Fri, 14 Dec 2001 11:51:01 +0100 wenzelm export add_tvarsT etc.;
Wed, 05 Dec 2001 03:09:21 +0100 wenzelm added add_rule, del_rule;
Mon, 26 Nov 2001 18:33:21 +0100 wenzelm added remdups_rl;
Sat, 24 Nov 2001 16:55:00 +0100 wenzelm gen_merge_lists';
Fri, 16 Nov 2001 15:24:09 +0100 wenzelm local_standard: plain strip_shyps instead of strip_shyps_warning;
Sun, 11 Nov 2001 21:30:10 +0100 wenzelm added conj_elim_precise, conj_intr_thm;
Fri, 09 Nov 2001 10:26:16 +0100 berghofe Theorems symmetric, reflexive and transitive are now stored with "open"
Wed, 07 Nov 2001 18:17:45 +0100 wenzelm tuned impose_hyps;
Mon, 05 Nov 2001 20:58:28 +0100 wenzelm export add_tvarsT, add_tvars, add_vars, add_frees (would actually
Wed, 31 Oct 2001 21:59:25 +0100 wenzelm added local_standard;
Wed, 31 Oct 2001 19:32:05 +0100 berghofe norm_hhf_eq is now stored using open_store_standard_thm.
Sun, 28 Oct 2001 19:44:58 +0100 wenzelm rules for meta-level conjunction;
Sat, 27 Oct 2001 00:06:46 +0200 wenzelm added impose_hyps;
Tue, 16 Oct 2001 23:00:21 +0200 wenzelm added implies_intr_goals;
Sat, 13 Oct 2001 20:32:07 +0200 wenzelm generic theorem kinds ("theorem", "lemma" etc.);
Fri, 31 Aug 2001 16:07:56 +0200 berghofe Some basic rules are now stored with "open" derivations, to facilitate
Tue, 20 Feb 2001 18:47:22 +0100 oheimb added rearrange_prems
Wed, 14 Feb 2001 19:27:49 +0100 berghofe imp_cong2 -> imp_cong
Sun, 07 Jan 2001 21:35:11 +0100 wenzelm removed outdated comment;
Wed, 03 Jan 2001 21:18:31 +0100 wenzelm Thm: dest_comb, dest_abs, capply, cabs no longer global;
Wed, 13 Dec 2000 17:43:33 +0100 wenzelm eliminated GOAL syntax;
Thu, 23 Nov 2000 21:29:50 +0100 wenzelm standard: close_derivation;
Fri, 10 Nov 2000 19:09:40 +0100 wenzelm store_standard_thm "norm_hhf_eq";
Tue, 07 Nov 2000 17:48:25 +0100 berghofe - new theorems imp_cong and swap_prems_eq
Mon, 06 Nov 2000 22:50:01 +0100 wenzelm Sign.typ_instance;
Tue, 05 Sep 2000 18:50:52 +0200 wenzelm improved add_rules;
Mon, 04 Sep 2000 21:18:28 +0200 wenzelm added add_rules, del_rules;
Tue, 08 Aug 2000 01:26:34 +0200 wenzelm added forall_elim_vars_safe, norm_hhf_eq;
Mon, 07 Aug 2000 10:29:04 +0200 paulson more cterm operations: mk_implies, list_implies
Sun, 30 Jul 2000 12:48:55 +0200 wenzelm Logic.goal_const;
Thu, 27 Jul 2000 18:27:09 +0200 wenzelm export has_internal;
Mon, 24 Jul 2000 23:47:14 +0200 wenzelm Drule.merge_rules;
Wed, 12 Jul 2000 16:44:34 +0200 wenzelm infix 'OF' is a version of 'MRS' with more appropriate argument order;
Thu, 30 Mar 2000 14:15:41 +0200 wenzelm added tvars_intr_list;
Wed, 22 Mar 2000 12:33:34 +0100 paulson new meta-rule "inst", a shorthand for read_instantiate_sg
Fri, 17 Mar 2000 16:28:59 +0100 wenzelm untag: remove all tags of given name;
Fri, 10 Mar 2000 14:57:06 +0100 berghofe Type.unify and Type.typ_match now use Vartab instead of association lists.
Wed, 08 Mar 2000 17:49:28 +0100 wenzelm added (un)tag_rule;
Thu, 02 Mar 2000 18:18:10 +0100 wenzelm added freeze_all;
Mon, 17 Jan 2000 14:10:32 +0100 paulson Thm.instantiate no longer normalizes, but Drule.instantiate does
Wed, 05 Jan 2000 11:35:18 +0100 wenzelm TypeInfer.logicT;
Thu, 21 Oct 1999 18:41:51 +0200 wenzelm forall_elim_var(s) moved to pure_thy.ML;
Wed, 29 Sep 1999 13:50:48 +0200 wenzelm strip_shyps_warning;
Sat, 04 Sep 1999 20:59:33 +0200 wenzelm handle Bind!!
Wed, 01 Sep 1999 21:04:01 +0200 wenzelm PureThy.smart_store_thms;
less more (0) -100 -60 tip