added world map

pre_cnf_tac: beta-eta-normalization restricted to the current subgoal

improvments in mail obfuscator

converted to isar theory; removed unsound adm_all axiom

update to reflect changes in inverts/injects lemmas

inverts and injects generated lemmas now take the form of rewrite rules, instead of dest rules

added lemma fresh_right, which is useful in the proof of the recursion combinator

added the_theory;

extend/remove_syntax: observe inout flag for translations, too;

handle exception SYS_ERROR;

abbreviation: observe local syntax mode;

added set_syntax_mode, restore_syntax_mode;

sys_error: exception SYS_ERROR;

maintain implicit syntax mode; tuned;

ThyInfo.the_theory;

ThyInfo.the_theory; tuned;

actually removed old stuff;

replaced syntax/translations by abbreviation; tuned proofs;

replaced syntax/translations by abbreviation;

replaced syntax/translations by abbreviation; tuned proofs; tuned;

beta_eta_conversion added to pre_cnf_tac

added obfuscation for mails

tidied and harmonized "params_of_state"

tuned;

tuned;

added domain_error; added of_sort_derivation; tuned;

of_sort: option; of_sort: simplified implementation, use Sorts.of_sort_derivation; tuned;

some facts about min, max and add, diff

a few more examples

class_triv: Sign.certify_class;

arities: maintain original codomain;

added sort_triv;

of_sort: simplified derivation;

adapted arities;

add theorem flift2_defined_iff

add theorem typdef_flat

AxClass.define_class_i, AxClass.get_definition; Sign.primitive_arity;

tuned;

AxClass.define_class; AxClass.axiomatize_class/classrel/arity;

build classes/arities: refer to operations in sorts.ML; simplified add_class/classrel/arity; tuned;

moved certify_class/sort to type.ML; added operations to build sort algebras (from type.ML); tuned;

removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity); added primitive_class/classrel/arity;

added serial_string;

renamed add_axclass(_i) to define_axclass(_i); renamed get_info to get_definition; added axiomatize_class/classrel/arity (supercede Sign.add_classes/classrel/arities); tuned;

AxClass.axiomatize_arity_i;

AxClass.define_class_i;

* Pure: axclasses now purely definitional; * Pure/kernel: consts certification ignores sort constraints;

reduced code duplication;

added insert_list;

added unconstrainT;

added unconstrainTs;

instances data: mutable cache; added of_sort: interface for derived instances;

tuned;

Capitalized theory names.

Removed broken proof.

Added Class, Fsub, and Lambda_mu examples for nominal datatypes.

New keyword file for HOL nominal datatype package.

Added new targets for nominal datatype package.

Capitalized theory names.

New ROOT file for nominal datatype examples.

Renamed "nominal" theory to "Nominal".

New ROOT file for nominal datatype package.

added some helper files for HOL goals/lemmas. Clauses have TPTP format.

changed the functions for getting HOL helper clauses.

removed the functions for getting HOL helper paths.

SplitAt -> chop

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;

'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.