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;
Thu, 27 Jul 2006 13:43:12 +0200 wenzelm added legacy_pretty_thm (with fall-back on ProtoPure.thy);
Thu, 27 Jul 2006 13:43:11 +0200 wenzelm Assumption.assume;
Thu, 27 Jul 2006 13:43:10 +0200 wenzelm removed obsolete is_fact (cf. Thm.no_prems);
Thu, 27 Jul 2006 13:43:09 +0200 wenzelm tuned interfaces;
Thu, 27 Jul 2006 13:43:08 +0200 wenzelm read_def_cterms (legacy version): Consts.certify;
Thu, 27 Jul 2006 13:43:07 +0200 wenzelm Assumption.assume;
Thu, 27 Jul 2006 13:43:06 +0200 wenzelm moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
Thu, 27 Jul 2006 13:43:05 +0200 wenzelm removed obsolete equal_abs_elim(_list);
Thu, 27 Jul 2006 13:43:04 +0200 wenzelm removed obsolete pretty_thm_no_quote;
Thu, 27 Jul 2006 13:43:03 +0200 wenzelm added Pure/assumption.ML;
Thu, 27 Jul 2006 13:43:01 +0200 wenzelm moved basic assumption operations from structure ProofContext to Assumption;
Thu, 27 Jul 2006 13:43:00 +0200 wenzelm tuned proofs;
Thu, 27 Jul 2006 13:42:59 +0200 wenzelm Local assumptions, parameterized by export rules.
Wed, 26 Jul 2006 19:37:44 +0200 wenzelm updated;
Wed, 26 Jul 2006 19:37:43 +0200 wenzelm import(T): result includes fixed types/terms;
Wed, 26 Jul 2006 19:37:42 +0200 wenzelm focus: result record includes (fixed) schematic variables;
Wed, 26 Jul 2006 19:37:41 +0200 wenzelm Variable.import(T): result includes fixed types/terms;
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Wed, 26 Jul 2006 13:31:07 +0200 haftmann added eval_term
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip