Adapted to new interface of add_axclass_i.

added zip/take/drop lemmas

tuned;

renamed Source.mapfilter to Source.map_filter;

added map_filter;

renamed mapfilter to map_filter, made pervasive (again); made flat pervasive (again); added maps;

tuned basic list operators (flat, maps, map_filter);

renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum

slight shortening of blacklist

cosmetic changes

some new functions

isar-keywords.el - I am not sure what has changed here nominal.thy - includes a number of new lemmas (including freshness and perm_aux things) nominal_atoms.ML - no particular changes here nominal_permeq.ML - a new version of the decision procedure using for permutation composition the constant perm_aux examples - various adjustments

*** empty log message ***

curried Seq.cons;

removed splitAt (superceded by chop); removed if_none (superceded by the_default);

tuned;

removed obsolete expand_case_tac;

fixed silly symlink bug

added Ben Porter's stuff

moved arithmetic series to geometric series in SetInterval

Sign.arity_sorts; tuned;

unlocalize_mixfix: fallback on NoSyn;

tuned;

refer to structure Type instead of Sorts;

added inter_sort; added arity_number/sorts;

added remove_sort;

added arity_number/sorts; tuned;

made 'flat' pervasive (again);

get_info: removed 'super' field; added params_of, all_params_of; removed params_of_sort; tuned;

seperated typedef codegen from main code

more precise tactics

fixed typo

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;