lin_arith_prover splits certain operators (e.g. min, max, abs)

lin_arith_prover splits certain operators (e.g. min, max, abs)

Only ignore too general axiom clauses, if the translation is partial- or constant-typed.

type annotations fixed (IntInf.int, to make SML/NJ happy)

lin_arith_prover splits certain operators (e.g. min, max, abs)

proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust

comment (timing information for last example) added

possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed

removed skip

Added in code to check too general axiom clauses.

exported attrib;

lin_arith_prover splits certain operators (e.g. min, max, abs)

fixed a bug in function poly: decomposition of products

Function package can now do automatic splits of overlapping datatype patterns

Removed an "apply arith" where there are already "No Subgoals"

code reformatted

Additional freshness constraints for FCB.

proper Element.generalize_facts;

add_consts: proper Sign.full_name; sortcontext_of_typ: avoid freeze_thaw, tuned;

added generalize_facts; tuned;

added maxidx_values;

export: refrain from adjusting maxidx;

adjust_maxidx: pass explicit lower bound; tuned interfaces;

Thm.adjust_maxidx;

removed unused add_in_order/add_once (cf. OrdList.insert);

demod_rule: depend on context, proper Variable.import/export;

tuned proofs;

lin_arith_prover splits certain operators (e.g. min, max, abs)

bugfix related to cancel_div_mod simproc

lin_arith_prover splits certain operators (e.g. min, max, abs)

rename legacy_pretty_thm to pretty_thm_legacy;

tuned comment;

added add_fixes_direct; tuned;

prove: proper assumption context, more tactic arguments; tuned;

added mk_conjunction_list;

Goal.prove: more tactic arguments;

Checking for unsound proofs. Tidying.

"all theorems" mode forces definition-expansion off. signature tidying

title fixed

replaced extern_skolem by slightly more simplistic revert_skolems; moved fix_frees to variable.ML;

renamed ProofContext.fix_frees to Variable.fix_frees;

replaced ProofContext.extern_skolem by slightly more simplistic ProofContext.revert_skolems;

no_vars: based on Variable.import; tuned;

added fix_frees (from Isar/proof_context.ML);

declare_term_names: cover types as well; removed unused zero_var_indexesT; tuned;

eliminated obsolete freeze_thaw;

type annotation added to make SML/NJ happy

"moved basic assumption operations from structure ProofContext to Assumption;"

ProofContext.legacy_pretty_thm;

added legacy_pretty_thm (with fall-back on ProtoPure.thy); moved basic assumption operations to assumption.ML; tuned;

Assumption.assume; moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);

removed obsolete is_fact (cf. Thm.no_prems);

tuned interfaces; moved basic assumption operations from structure ProofContext to Assumption;

read_def_cterms (legacy version): Consts.certify;

Assumption.assume;

moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);

removed obsolete equal_abs_elim(_list);

removed obsolete pretty_thm_no_quote;

added Pure/assumption.ML;

moved basic assumption operations from structure ProofContext to Assumption;

tuned proofs;

Local assumptions, parameterized by export rules.

updated;

import(T): result includes fixed types/terms; focus: tuned interface;

focus: result record includes (fixed) schematic variables; SUBGOAL: disallow pending subgoals, more robust re-composition;

Variable.import(T): result includes fixed types/terms;

linear arithmetic splits certain operators (e.g. min, max, abs)

added eval_term

updated;

fixed LaTeX problem;

added eval_term

Removed wrong sentence (Simon Funke)

moved pprint functions to Isar/proof_display.ML;

Tactical operations depending on local subgoal structure.

moved pprint functions to Isar/proof_display.ML; added primitive add_assumes; tuned internal prems: no names;

export goal_tac (was internal refine_tac);

added Pure/subgoal.ML;

updated;

raw symbols: disallow dot to avoid confusion in NameSpace.unpack;

avoid Term.is_funtype;

avoid structure Char;

added variant_abs (from term.ML); tuned;

added find_free (from term.ML);

added is/to_ascii_lower/upper; tuned alphanum -- needs more work;

is_funtype: do not export internal operation; added add_varnames (cf. add_vars etc.); removed obsolete (add_)term_varnames; removed find_free (moved to Isar/obtain.ML); moved variant_abs to structure Syntax -- this is a syntax operation after all;

tuned;

use Term.add_vars instead of obsolete term_varnames;

renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);

tuned ML code;

renamed Term.variant_abs to Syntax.variant_abs;

Drule.merge_rules;

renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum

improvements for lazy code generation

fixed typo

added code generator serialization for Char

added notes on class_package.ML and codegen_package.ML

small adjustments

fixed bug for serialization for uminus on ints

small improvement in serialization for wfrec

added structure HOList

major simplifications for integers

tactic for prove_instance_arity now gets definition theorems as arguments

added term_of_string function

simplification for code generation for Integers

adaption to argument change in primrec_package

adaption to changes in class_package

hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen

exported equation transformator

class package and codegen refinements

added give_names and alphanum

Some cases in "case ... of ..." expressions may now be omitted (internally, these cases are assigned the "undefined" value).

- Added new "undefined" constant - normalization_conv no longer expects term to have form "Trueprop ..."

removed Variable.monomorphic;

comments fixed, member function renamed

Change to algebra method.

Reimplemented algebra method; now controlled by attribute.

Strict dfs traversal of imported and registered identifiers.

added map_default, internal restructuring

export is_tid;

thm_of_proof: improved generation of variables;