added code_constname keyword

fixed code generator theorem generation

improvements for 2nd codegenerator

cleanup code generation for Numerals

improved & fixed code generator theorem generation

code generator refinements

adding code lemma now works as expected

added more examples

dropped duplicated line

added Tools/typedef_codegen.ML

abandoned equal_list in favor for eq_list

Simple ML script for producing Gnuplot files from isatest log files.

title fixed

updated;

avoid low-level tsig;

reworked read_instantiate -- separate read_insts;

tuned;

removed obsolete sign_of;

Amine Chaieb: experimental generic reflection and reification in HOL;

use atbroy101 instead of atbroy98 (freezes up)

Added Keywords: "otherwise" and "sequential", needed for function package's sequential mode.

*** empty log message ***

Rule instantiations -- operations within a rule/subgoal context.

moved bires_inst_tac etc. to rule_insts.ML;

moved read_instantiate etc. to rule_insts.ML;

added Isar/rule_insts.ML;

removed obsolete commute, map_list;

removed obsolete add_term_tvarnames;

tuned;

tuned types_sorts, add_used;

RuleInsts.bires_inst_tac;

*** empty log message ***

fixed generator

added HOL/ex/Reflection;

removed True_implies (cf. True_implies_equals); added header;

removed OldGoals.legacy flag (always warn); added warning for legacy ML scripts;

removed OldGoals.legacy flag (always warn);

tuned;

removed True_implies (cf. True_implies_equals);

Generic reflection and reification (by Amine Chaieb).

Restructured algebra library, added ideals and quotient rings.

Updated comments.

updated;

tuned proofs;

lemma da_good_approx: adapted induction (was exploting lifted obtain result);

renamed Syntax.indexname to Syntax.read_indexname; added read_int (not Int.fromString, which admits ~ syntax of ML);

tuned;

moved debug option to proof_display.ML (again); normalized Proof.context/method type aliases;

normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; prems_limit: < 0 means no output; added debug option (back from proof_display.ML);

simplified Assumption/ProofContext.export; simplified end_block;

added tactical result; simplified obtain_export: no Seq.seq, no lifting of result prems; tuned;

removed obsolete Drule.frees/vars_of etc.; simplified Assumption/ProofContext.export;

normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export;

simplified Proof.end_block;

removed obsolete Drule.frees/vars_of etc.; tuned;

normalized Proof.context/method type aliases; added declare/export/import_prf; added focus_subgoal: reset/declare goal schematics;

renamed Syntax.indexname to Syntax.read_indexname;

Variable.focus_subgoal;

replaced maxidx_of_proof by maxidx_proof;

prems-limit: int_option;

removed obsolete frees/vars_of etc.; removed obsolete freeze_all etc.; added norm_hhf_cterm; tuned fold_terms; renamed Syntax.indexname to Syntax.read_indexname;

fake predeclaration of type Proof.context;

simplified export: no Seq.seq; normalized Proof.context/method type aliases;

use proper RecdefPackage.get_hints; tuned;

removed obsolete Drule.frees/vars_of; renamed thm_vars to thm_varnames;

renamed thm_vars to thm_varnames;

removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;

export get_hints; tuned;

normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; tuned;

normalized Proof.context/method type aliases;

simplified Assumption/ProofContext.export;

replaced obsolete standard/freeze_all by Variable.trade;

removed obsolete Drule.frees/vars_of etc.;

Added type constraint to please sml/nj

deleted obsolete file

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.