-- terms are fully typed. -- only the top-level boolean terms are predicates.

-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.

-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.

-- added combinator reduction axioms (typed and untyped) for HOL goals. -- combined make_nnf functions for HOL and FOL goals. -- hypothesis of goals are now also skolemized by inference.

-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).

-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.

-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL. -- added "check_is_fol_term", which is the same as "check_is_fol", but takes a "term" as input. -- added "check_is_fol" and "check_is_fol_term" into the signature.

tuned document;

tuned;

improved induction proof: local defs/fixes;

tuned Pattern.match/unify; tuned fold;

added deskolem;

added THEN_ALL_NEW_CASES; Syntax.deskolem;

added revert_skolem, mk_def, add_def; export: Goal.norm_hhf'; tuned;

ProofContext.mk_def;

Term.betapplys;

tuned Pattern.match/unify;

added betapplys;

tuned interfaces to support incremental match/unify (cf. versions in type.ML);

tuned;

norm_hhf: no normalization of protected props;

added protect_cong, cong_mono_thm; outer_params: Syntax.deskolem;

induct: support local definitions to be passed through the induction; deprecate open rule cases; misc cleanup;

Trueprop: use ObjectLogic.judgment etc.; uniform Const of name * typargs, removed TConst;

Term.betapply;

new version of "tryres" allowing multiple unifiers (apparently needed for Skolemization of higher-order theorems)

pgmlsymbolson: append Symbol.xsymbolsN at end!

better no -d option;

added generic transformators

removal of is_hol

added module system

added modules for code generator generation two, not operational yet

class_package - operational view on type classes

string_of_alist - convenient q'n'd printout function

support for polyml-4.2.0;

new syntax for class_package

added const_instance;

added instance;

added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;

Compatibility wrapper for Poly/ML 4.2.0.

tuned;

added a few equivariance lemmas (they need to be automated eventually)

changed the HOL_basic_ss back and selectively added simp_thms and triv_forall_equality. (Otherwise the goals would have been simplified too much)

exchanged HOL_ss for HOL_basic_ss in the simplification part. Otherwise the case where the context is instantiated with unit leads to vacuous quantifiers, such as ALL a. A

a proof step corrected due to the changement in the presburger method.

old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.

add header

tuned proofs;

moved find_free to term.ML;

guess: Seq.hd; Term.find_free;

guess: Toplevel.proof;

added find_free (from Isar/proof_context.ML);

curried multiply;

induct method: fixes; tuned;

uncurried Consts.typargs;

renamed Thm.cgoal_of to Thm.cprem_of;

duplicate axioms in ATP linkup, and general fixes

tidying

called the induction principle "unsafe" instead of "test".

Skolemization by inference, but not quite finished

Explicit data structures for some Isar language elements.

tuned;

tvars_intr_list: natural argument order;

moved datatype elem to element.ML; removed unused imports function;

P.context_element, P.locale_element;

Element.context;

use existing exeption Empty;

avoid code redundancy; tuned comments;

tuned comments;

removed obsolete term set operations;

P.locale_element;

added fold_terms; added tfrees_of, frees_of; tvars_intr_list: natural argument order;

added Isar/element.ML;

Thm.varifyT': natural argument order;

added join function

allowing indentation of 'theory' keyword

simplified after_qed;

avoid prove_plain, export_plain, simplified after_qed; witness = term * thm, i.e. the original proposition with a protected fact (this achieves reliable discharge and allows facts to be slightly more general/normalized); internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly; ObjectLogic.ensure_propT;

removed export_plain; (some_)fact_tac: Drule.incr_indexes;

renamed assert_prop to ensure_prop;

renamed goals.ML to old_goals.ML; inline Drule.impose_hyps;

export compose_hhf; removed obsolete norm_hhf_plain; tuned;

removed impose_hyps, satisfy_hyps; tuned;

const args: do not store variable names (unused);

renamed goals.ML to old_goals.ML;

(fix for accidental commit)

(codegen)

generate pattern combinators for new datatypes

reimplemented Case syntax using print/parse translations; moved as-patterns to separate section

add case syntax for type one

remove syntax for as-patterns

avoid 'as' as identifier;

avoid 'as' as identifier;

Added strong induction theorem (currently only axiomatized!).

Initial commit.

Initial commit of the theory "Weakening".