more precise data structure

cleaned up some diagnostic mathom

moved coalesce to AList, added equality predicates to library

added LP.thy

Changed the treatment of equalities.

Changed the logic detection method.

exported linkup_logic_mode and changed the default setting

fix to spacing in switches, for Vampire under SML/NJ

definition expansion checks for excess variables

the "th" field of type "clause"

tidying and reformatting

tidying; ATP options including CASC mode for Vampire

Take conjectures and axioms as thms when convert them to ResHolClause.clause format.

Take conjectures and axioms as thms when convert them to ResClause.clause format.

Tidied up some programs.

fixed typo

add lemma less_UU_iff as default simp rule

hide common name of constant 'run'

early test of Classpackage, Codegenerator;

fixed typo in method invocation;

ignore sort constraints of consts declarations; use conjunction stuff from conjunction.ML; prefer ProofContext.pretty_thm;

ignore sort constraints of consts declarations; Sign.typ_equiv;

add_axclass(_i): canonical specification format;

certify: ignore sort constraints of declarations (MAJOR CHANGE);

added print_theorems/theory, print_theorems_diff (from pure_thy.ML);

axclass: old-style concrete syntax for canonical specification format;

ProofDisplay.print_theorems/theory;

added maxidx_of;

tuned;

added typ_equiv; read_class: improved error;

moved print_theorems/theory to Isar/proof_display.ML;

added dest_conjunction_list; close_form: canonical order of variables;

export unflat (again);

use conjunction stuff from conjunction.ML;

expand_atom: Type.raw_match;

added equal_elim_rule2; export dest_binop; export store_thm etc; moved conjunction stuff to conjunction.ML;

tuned comment;

ignore sorts of consts declarations;

reworded add_axclass(_i): canonical specification format, purely definitional version, always qualify intro/axioms;

added conjunction.ML;

Meta-level conjunction.

added conjunction.ML; tuned;

Sign.typ_equiv;

added subversion treatment

classes: prefer thy operations; accomodate tuned interfaces of Logic/Sign/AxClass;

export pretty_classrel/arity;

'axclass': no parameters;

tuned;

removed superclasses (see sign.ML);

added super_classes (from sorts.ML); removed read/cert_classrel (see axclass.ML);

added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML); tuned;

moved abstract syntax operations to logic.ML; maintain class parameters; added params_of_sort; added cert/read_classrel (from sign.ML), check class parameters; tuned;

Moved stuff from Ring_and_Field to Matrix

Adapted to changed type of add_typedef_i.

Hoare(Parallel) dependencies on document/*

added references

Minimal doc

Included cyclic list examples

fixed value restriction

Added splicing algorithm.

hide (open) const;

simplified AxClass.add_axclass interface;

added aT (from axclass.ML); non-pervasive itselfT, a_itselfT;

removed unused class_le_path, sort_less;

add_axclass(_i): return class name only; subclass/arity statements: require actual TVars, store raw data; tuned;

Term.itselfT;

Added function "splice"

Even/Odd: avoid clash with even/odd of Main HOL;

results: smart_pretty_thm uses adhoc proof context if possible;

added full_name; abbrevs: mode does not affect name space;

add_syntax: actually observe print mode;

print_term etc.: actually observe print mode in final output;

abbrevs: mode does not affect name space;

added coalesce;

moved theory presentation to Isar/ROOT.ML;

hide consts in Numeral.thy;

tuned syntax/abbreviations;

unfold(ed): not necessrily meta equations;

Made "empty" an abbreviation.

*** empty log message ***

Removed old set interval syntax.

pretty_term: late externing of consts (support authentic syntax);

pretty: late externing of consts (support authentic syntax);

removed fix_mixfix; added const_mixfix, mixfix_const;

abbreviation(_i): do not expand abbreviations, do not use derived_def;

add_abbrevs(_i): support print mode; pretty_term': expand abbreviations only for well-typed terms; added expand_abbrevs; tuned;

abbrevs: support print mode;

simplified handling of authentic syntax (cf. early externing in consts.ML); simplified extern_term;

'abbreviation': optional print mode;

tuned;

pretty_term': early vs. late externing (support authentic syntax); add_abbrevs(_i): support print mode and authentic syntax;

print_theory: print abbreviations nicely;

added intern/extern/extern_early; added expand_abbrevs flag; strip_abss: demand ocurrences of bounds in body; const decl: added flag for early externing (disabled for authentic syntax); abbrevs: support print mode; major cleanup;

refined 'abbreviation';

made symlink relative

made symlink relative

converted Müller to Mueller to make smlnj 110.58 work

Fixed bug that caused proof of induction rule to fail for inductive sets with trivial introduction rules such as "x : S ==> x : S".

remame ASeries to Arithmetic_Series

Added alternative version of thms_of_proof that does not recursively descend into proofs of (named) theorems.

hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.

filter now accepts axioms as thm, instead of term.

tptp_write_file accepts axioms as thm.

added another function for CNF.

lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.

renamed ASeries to Arithmetic_Series, removed the ^M

modified the perm_compose rule such that it is applied as simplification rule (as simproc) in the restricted case where the first permutation is a swapping coming from a supports problem also deleted the perm_compose' rule from the set of rules that are automatically tried

cleanup in typedef/datatype package

added explicit serialization for int equality

adapted for definitional code generation

cleanup in datatype package

small type annotation fix

added hook for codegen_theorems.ML

adaptions to change in typedef_package.ML

added functions for definitional code generation

added definitional code generator module: codegen_theorems.ML

minor changes

exported specification names

minor extensions

pool of constants; definition expansion; current best settings

removed some illegal characters: they were crashing SML/NJ

Removal of unused code

Simplified version of Jia's filter. Now all constants are pooled, rather than relevance being compared against separate clauses. Rejects are no longer noted, and units cannot be added at the end.

renamed map_val to map_ran

added map_val, superseding map_at and substitute ----------------------------------------------------------------------

some internal cleanup

removed illegal character codes

simplified the proof at_fin_set_supp

changed abbreviation for "infinite" back to translation because something didn't work during (output).

lazy patterns in lambda abstractions

changed the it_prm proof to work for recursion

tuned some proofs

Removed occurrences of makestring, which does not exist in SML/NJ.

Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.

Replaced iteration combinator by recursion combinator.

detection of definitions of relevant constants

Only display atpset theorems if Output.show_debug_msgs is true.

added the first two simple proofs of the recursion combinator

comment fixed

Introduction of "whitelist": theorems forced past the relevance filter

Slight simplification of proofs

Removal of obsolete strategies. Initial support for locales: Frees and Consts treated similarly.

comment for conjI added

translations -> abbreviations (a cool feature)

fixed example;

mark_boundT: produce well-typed term;

subtract (op =); pretty_proof: no abbrevs;

avoid polymorphic equality; tuned;

avoid polymorphic equality; subtract (op =);

moved gen_eq_set to library.ML;

added ~$$ (negative literal); combinators: avoid code duplication; tuned extend_lexicon;

avoid polymorphic equality;

remove (op =); tuned;

gen_eq_set, remove (op =);

abbreviation upto, length;

added subtract; tuned;

subtract (op =);

remove (op =);

Now SML/NJ-friendly (IntInf)

Removal of unnecessary simprules: simproc cancel_numerals now works without add_Suc, while the reason for the horrible isolateSuc is not known.

interpret: Proof.assert_forward_or_chain;

subsetI is often necessary

Now the setup for cancel_numerals accepts mixed Sucs/+ where the Sucs no longer need to be outermost.

Tuned signature of Locale.add_locale(_i).

simplified mg_domain (use Sign.classes/arities_of); removed unused lift_local_theory_yield;

made $$ and "this" monomorphic (string);

tuned;

export arities_of instead of classes_arities_of;

updated;

renamed const less to lt;

renamed constant less in lattice

fixed problem with proof reconstruction by adding add_Suc to arith-simpset.

added parser locale_expr_unless

fixed clsvar bug

add_locale(_i) returns internal locale name.

added example for operational classes and code generator

slight improvement in serializer, stub for code generator theorems added

Renamed setsum_mult to setsum_right_distrib.

Internal restructuring: local parameters.

renamed op < <= to Orderings.less(_eq)

New interface function parameters_of_expr.

add_inst_arity_i renamed to prove_arity.

rename_frees: treat trivial names; monomorphic: tuned invented names;

added singleton;

updated;

turned string_of_mixfix into pretty_mixfix;

added monomorphic; export hidden_polymorphism;

added 'print_statement' command;

added print_stmts;

added pretty_statement;

added command, keyword; added chunks2;

Output.add_mode: keyword component;

string_of_mixfix;

print_statement;

added remove_trrules(_i); tuned;

added is_elim (from Provers/classical.ML);

added 'no_translations';

added pretty_stmt; tuned;

declared_const: check for type constraint only, i.e. admit abbreviations as well; added del_trrules(_i);

ObjectLogic.is_elim;

tuned constdecl; added 'no_translations';

updated;

Pure: no_translations;

refined representation of instance dictionaries

entry for Library/AssocList

First version of function for defining graph of iteration combinator.

got rid of type Sign.sg;

renamed plus to add;

renamed const minus to subtract;

simplified AxClass interfaces;

added axclass_instance_XXX (from axclass.ML); Sign.read/cert_arity;

*** empty log message ***

added read_class, read/cert_classrel/arity (from axclass.ML);

moved read_class, read/cert_classrel/arity to sign.ML; axclass: moved outer syntax to isar_syn.ML; instance: moved to Tools/class_package.ML; simplified interfaces; tuned;

use axclass.ML earlier (in Isar/ROOT.ML);

nbe: no_document;

tuned;

exporting reapAll and killChild

text delimiter fixed

comment delimiter fixed

clauses now use (meta-)hyps instead of (meta-)implications; significant speedup

fix for document preparation

Added Library/AssocList.thy

renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.

Changed some warnings to debug messages

Frequency analysis of constants (with types). Ability to restrict the number of accepted clauses.

Shortened the exception messages from assume.

METAHYPS catches THM assume exception and prints out the terms containing schematic vars.

added many simple lemmas

Added more functions to the signature and tidied up some functions.

tuned;

tuned some proofs

select_goals: split original conjunctions;

method: goal restriction defaults to [1];

infer_derivs: avoid allocating empty MinProof;

tuned;

Isar/method: goal restriction;

constdecl: always allow 'where';

deleted some proofs "on comment"

tuned some proofs