Wed, 02 Aug 2006 22:26:48 +0200 wenzelm removed obsolete Drule.frees/vars_of;
Wed, 02 Aug 2006 22:26:47 +0200 wenzelm renamed thm_vars to thm_varnames;
Wed, 02 Aug 2006 22:26:46 +0200 wenzelm removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;
Wed, 02 Aug 2006 22:26:45 +0200 wenzelm export get_hints;
Wed, 02 Aug 2006 22:26:44 +0200 wenzelm normalized Proof.context/method type aliases;
Wed, 02 Aug 2006 22:26:41 +0200 wenzelm normalized Proof.context/method type aliases;
Wed, 02 Aug 2006 22:26:40 +0200 wenzelm simplified Assumption/ProofContext.export;
Wed, 02 Aug 2006 22:26:39 +0200 wenzelm replaced obsolete standard/freeze_all by Variable.trade;
Wed, 02 Aug 2006 22:26:37 +0200 wenzelm removed obsolete Drule.frees/vars_of etc.;
Wed, 02 Aug 2006 18:33:46 +0200 krauss Added type constraint to please sml/nj
Wed, 02 Aug 2006 18:30:57 +0200 paulson deleted obsolete file
Wed, 02 Aug 2006 18:19:48 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 02 Aug 2006 16:50:41 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 02 Aug 2006 13:48:21 +0200 mengj Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
Wed, 02 Aug 2006 03:33:28 +0200 webertj type annotations fixed (IntInf.int, to make SML/NJ happy)
Wed, 02 Aug 2006 01:48:09 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 02 Aug 2006 00:57:41 +0200 webertj proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
Tue, 01 Aug 2006 15:28:55 +0200 webertj comment (timing information for last example) added
Tue, 01 Aug 2006 14:58:43 +0200 webertj possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
Tue, 01 Aug 2006 13:51:16 +0200 obua removed skip
Tue, 01 Aug 2006 13:44:05 +0200 mengj Added in code to check too general axiom clauses.
Tue, 01 Aug 2006 11:32:43 +0200 wenzelm exported attrib;
Mon, 31 Jul 2006 21:06:40 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Mon, 31 Jul 2006 20:56:49 +0200 webertj fixed a bug in function poly: decomposition of products
Mon, 31 Jul 2006 18:07:42 +0200 krauss Function package can now do automatic splits of overlapping datatype patterns
Mon, 31 Jul 2006 18:05:40 +0200 krauss Removed an "apply arith" where there are already "No Subgoals"
Mon, 31 Jul 2006 15:29:36 +0200 webertj code reformatted
Mon, 31 Jul 2006 14:08:42 +0200 berghofe Additional freshness constraints for FCB.
Sun, 30 Jul 2006 21:28:59 +0200 wenzelm proper Element.generalize_facts;
Sun, 30 Jul 2006 21:28:58 +0200 wenzelm add_consts: proper Sign.full_name;
Sun, 30 Jul 2006 21:28:57 +0200 wenzelm added generalize_facts;
Sun, 30 Jul 2006 21:28:56 +0200 wenzelm added maxidx_values;
Sun, 30 Jul 2006 21:28:55 +0200 wenzelm export: refrain from adjusting maxidx;
Sun, 30 Jul 2006 21:28:54 +0200 wenzelm adjust_maxidx: pass explicit lower bound;
Sun, 30 Jul 2006 21:28:52 +0200 wenzelm Thm.adjust_maxidx;
Sun, 30 Jul 2006 21:28:51 +0200 wenzelm removed unused add_in_order/add_once (cf. OrdList.insert);
Sun, 30 Jul 2006 21:28:50 +0200 wenzelm demod_rule: depend on context, proper Variable.import/export;
Sun, 30 Jul 2006 21:28:48 +0200 wenzelm tuned proofs;
Sun, 30 Jul 2006 05:53:10 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Sun, 30 Jul 2006 02:06:01 +0200 webertj bugfix related to cancel_div_mod simproc
Sat, 29 Jul 2006 13:15:12 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Sat, 29 Jul 2006 00:51:36 +0200 wenzelm rename legacy_pretty_thm to pretty_thm_legacy;
Sat, 29 Jul 2006 00:51:34 +0200 wenzelm tuned comment;
Sat, 29 Jul 2006 00:51:33 +0200 wenzelm added add_fixes_direct;
Sat, 29 Jul 2006 00:51:32 +0200 wenzelm prove: proper assumption context, more tactic arguments;
Sat, 29 Jul 2006 00:51:31 +0200 wenzelm added mk_conjunction_list;
Sat, 29 Jul 2006 00:51:29 +0200 wenzelm Goal.prove: more tactic arguments;
Fri, 28 Jul 2006 18:37:25 +0200 paulson Checking for unsound proofs. Tidying.
Fri, 28 Jul 2006 18:36:24 +0200 paulson "all theorems" mode forces definition-expansion off.
Fri, 28 Jul 2006 18:11:22 +0200 webertj title fixed
Thu, 27 Jul 2006 23:28:30 +0200 wenzelm replaced extern_skolem by slightly more simplistic revert_skolems;
Thu, 27 Jul 2006 23:28:28 +0200 wenzelm renamed ProofContext.fix_frees to Variable.fix_frees;
Thu, 27 Jul 2006 23:28:27 +0200 wenzelm replaced ProofContext.extern_skolem by slightly more simplistic ProofContext.revert_skolems;
Thu, 27 Jul 2006 23:28:26 +0200 wenzelm no_vars: based on Variable.import;
Thu, 27 Jul 2006 23:28:25 +0200 wenzelm added fix_frees (from Isar/proof_context.ML);
Thu, 27 Jul 2006 23:28:23 +0200 wenzelm declare_term_names: cover types as well;
Thu, 27 Jul 2006 15:33:21 +0200 wenzelm eliminated obsolete freeze_thaw;
Thu, 27 Jul 2006 14:21:57 +0200 webertj type annotation added to make SML/NJ happy
Thu, 27 Jul 2006 13:44:03 +0200 wenzelm "moved basic assumption operations from structure ProofContext to Assumption;"
Thu, 27 Jul 2006 13:43:13 +0200 wenzelm ProofContext.legacy_pretty_thm;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip