2006-08-02 webertj type annotations fixed (IntInf.int, to make SML/NJ happy)
2006-08-01 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-08-01 webertj proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
2006-08-01 webertj comment (timing information for last example) added
2006-08-01 webertj possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
2006-08-01 obua removed skip
2006-08-01 mengj Added in code to check too general axiom clauses.
2006-08-01 wenzelm exported attrib;
2006-07-31 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-31 webertj fixed a bug in function poly: decomposition of products
2006-07-31 krauss Function package can now do automatic splits of overlapping datatype patterns
2006-07-31 krauss Removed an "apply arith" where there are already "No Subgoals"
2006-07-31 webertj code reformatted
2006-07-31 berghofe Additional freshness constraints for FCB.
2006-07-30 wenzelm proper Element.generalize_facts;
2006-07-30 wenzelm add_consts: proper Sign.full_name;
2006-07-30 wenzelm added generalize_facts;
2006-07-30 wenzelm added maxidx_values;
2006-07-30 wenzelm export: refrain from adjusting maxidx;
2006-07-30 wenzelm adjust_maxidx: pass explicit lower bound;
2006-07-30 wenzelm Thm.adjust_maxidx;
2006-07-30 wenzelm removed unused add_in_order/add_once (cf. OrdList.insert);
2006-07-30 wenzelm demod_rule: depend on context, proper Variable.import/export;
2006-07-30 wenzelm tuned proofs;
2006-07-30 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-30 webertj bugfix related to cancel_div_mod simproc
2006-07-29 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-28 wenzelm rename legacy_pretty_thm to pretty_thm_legacy;
2006-07-28 wenzelm tuned comment;
2006-07-28 wenzelm added add_fixes_direct;
2006-07-28 wenzelm prove: proper assumption context, more tactic arguments;
2006-07-28 wenzelm added mk_conjunction_list;
2006-07-28 wenzelm Goal.prove: more tactic arguments;
2006-07-28 paulson Checking for unsound proofs. Tidying.
2006-07-28 paulson "all theorems" mode forces definition-expansion off.
2006-07-28 webertj title fixed
2006-07-27 wenzelm replaced extern_skolem by slightly more simplistic revert_skolems;
2006-07-27 wenzelm renamed ProofContext.fix_frees to Variable.fix_frees;
2006-07-27 wenzelm replaced ProofContext.extern_skolem by slightly more simplistic ProofContext.revert_skolems;
2006-07-27 wenzelm no_vars: based on Variable.import;
2006-07-27 wenzelm added fix_frees (from Isar/proof_context.ML);
2006-07-27 wenzelm declare_term_names: cover types as well;
2006-07-27 wenzelm eliminated obsolete freeze_thaw;
2006-07-27 webertj type annotation added to make SML/NJ happy
2006-07-27 wenzelm "moved basic assumption operations from structure ProofContext to Assumption;"
2006-07-27 wenzelm ProofContext.legacy_pretty_thm;
2006-07-27 wenzelm added legacy_pretty_thm (with fall-back on ProtoPure.thy);
2006-07-27 wenzelm Assumption.assume;
2006-07-27 wenzelm removed obsolete is_fact (cf. Thm.no_prems);
2006-07-27 wenzelm tuned interfaces;
2006-07-27 wenzelm read_def_cterms (legacy version): Consts.certify;
2006-07-27 wenzelm Assumption.assume;
2006-07-27 wenzelm moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
2006-07-27 wenzelm removed obsolete equal_abs_elim(_list);
2006-07-27 wenzelm removed obsolete pretty_thm_no_quote;
2006-07-27 wenzelm added Pure/assumption.ML;
(0) -10000 -3000 -1000 -300 -100 -56 +56 +100 +300 +1000 +3000 +10000 +30000 tip