prove: full Variable.declare_term, including constraints;

prove_standard: more precises argument passing; proper context for tactics derived from res_inst_tac;

InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;

simplified InductTacs.case_tac/induct_tac;

tuned proof;

removed obsolete nat_induct_tac -- cannot work without;

removed obsolete case_split_tac -- cannot work without;

removed unused excluded_middle_tac; proper context for tactics derived from res_inst_tac; tuned setup;

updated geenrated file;

qualified old res_inst_tac variants;

proper context for tactics derived from res_inst_tac;

updated generated file;

obsolete;

certify_term: reject qualified frees;

removed experimental Poplog/PML support; removed obsolete ML_SUFFIX; some reformatting;

removed obsolete ML_SUFFIX; some reformatting;

removed experimental Poplog/PML support;

removed obsolete ML_SUFFIX;

removed exotic 'token_translation' command;

proper name for LinearQuantifierElim;

removed old theorem database;

map_const: soft version, no failure here (recovers hiding of consts, because a hidden name is illegal and rejected later);

hide: delete all accesses from extra names -- reduces ambiguity in extern;

map_const: soft version, no failure here;

skolem_fact/thm: uniform numbering, even for singleton list; declare_skofuns: eliminated recovery via Clausify_failure -- should be sufficiently robust as is;

hide (open);

no_notation instead of hide;

* Recovered hiding of consts;

updated generated file;

back to CodeTarget.code_width;

hide -> hide (open)

use regular error function;

add lemma finite_image_approx; remove unnecessary sort annotations

change orientation of fix_eqI and convert to rule_format; add lemma fix_ind2

export just one setup function; more antiquotations; to_nnf: import open, avoiding internal variables (bounds); ThmCache: added table of seen fact names; reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end; removed obsolete skolem attribute (NB: official fact name unavailable here);

removed obsolete skolem declarations -- done by Theory.at_end;

tuned setup;

remove unnecessary import of Ffun; add lemma admD2

imports Ffun

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context; eliminated obscure theory merge/transfer -- use explicit theory context instead;

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;

sane versions of (qualified_)thms_of_thy;

Facts.dest/export_static: content difference; tuned;

dest/export_static: content difference; tuned comments;

declare_skofuns/skolem: canonical argument order; minor tuning;

Facts.dest/export_static: content difference;

correction

tuned

Removed hide swap

fixed type

lemma modified

typo

had to add rule: because induct_tac no longer works correctly

Hid swap

some reformatting;

added CK_Machine to the nominal section

soundness and completeness proofs for a CK machine as well as proofs for type preservation

emoved the parts that deal with the CK machine to a new theory

tuned header and comments

OldGoals.inst;

Drule.read_instantiate; Drule.types_sorts;

qualified inst;

qualified types_sorts, read_insts etc.;

Drule.types_sorts;