Removed some polymorphic equality tests

Improved indentation of aconv

Corrected aeconv and exported it

Prevent permutation of assumptions in hyp_subst_tac

Deleted steps made redundant by the stronger eq_assume_tac

Eta-expanded some declarations for compatibility with value polymorphism

Tidied and updated

more robust check;

renamed, improved, augmented version of isabelle fonts;

tuned comment;

tuned;

pass xterm mode by default;

Minor changes due to primrec definition for ^

primrec definition for ^

Minor changes due to primrec definition for nth

primrec definition for nth

Oops, forgot to remove -x again;

added ISABELLE_HOME normalization;

even more robust and user friendly invocation (no longer requieres absolute path names);

improved DESCRIPTION;

added -a, -b options; multiple VARNAMES;

*** empty log message ***

*** empty log message ***

*** empty log message ***

Added comment

Now uses eta_contract_atom for greater speed

Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors

HOL: renaming of "not"

Declares eta_contract_atom; fixed comment; some tidying

Added comment

Now declares needs_filtered_use, but still unusable with current MLWorks

Now uses rotate_tac and eta_contract_atom for greater speed

New version of InterE, like its ZF counterpart

Renamed constant "not" to "Not"

Renamed constant "not" to "Not"

Renamed constant "not" to "Not"

best_tac avoids looping with change to RepFun_eqI in claset

Now uses RepFun_eqI instead of RepFunI; improved version of InterE to replace "make_elim InterD" in claset

Updated reference to Pelletier erratum

Removed needless quotes

removed bash debug;

removed -r option; added -p option;

fixed -m order;

improved xterm, xterm_color;

added comment;

added comment: print translations do not mark tokens;

added color styles; refs for test;

improved err msg;

*** empty log message ***

more robust handling of invocation errors; added -m MODE option;

more robust handling of invocation errors;

now uses -m symbols;

split ast_of_term(T); ast_of_term now marks frees; added token translation support;

added token translation support;

term_of_... now mark class, tfree, tvar;

added mark_bound(T), variant_abs'; trfuns now mark bounds they introduce!! added pure_trfunsT;

Token translations for xterm and LaTeX output.

added _mk_ofclass(S);

added strlen (includes metric information); removed map_strs;

added token_translation interface;

added add_tokentrfuns;

added Syntax/token_trans.ML;

added token_trans.ML;

Slightly more robust proof

dup_intr & dup_elim no longer call standard -- this lets them be used on meta-hyps

rule_by_tactic no longer standardizes its result

Addition of de Bruijn formulae

tuned comment;

tuned comments;

added proper subset symbols syntax;

minor changes due to primrec defintions for +,-,*

minor changes due to new primrec definitions for +,-,*

definitions of +,-,* replaced by primrec definitions

function nat_add_primrec added to allow primrec definitions over nat

removed explicit_domains/, which is now covered by ex/

added "_" syntax for dummyT;

declared the dummy type;

replaced natural by subset;

tuned symbolic [|_|] syntax;

tuned some chars;

More robust proof (?)

Replaced "flat" by the Basis Library function List.concat

Introduction of rotate_rule

removed empty line (which broke xfedor);

don't hack, use xfed or xfedor;

fixed Id comment;

makedist -- make Isabelle distribution.

tuned URL;

added index info;

index info;

added dist;

some administrative tools for the Isabelle;

made a bit more robust for 'make dist';

rail output;

fixed rail.sty dep;

added this file;

rail output;

made a bit more robust;

manual steps comment;

*** empty log message ***

described changes for HOLCF-Version without rules and arities

file moved;

file moved here;

configure - adapt Isabelle distribution to system environment

improved description of recent changes

reflecting recent changes of the simplifier

corrected type of plift

reflecting recent changes of the simplifier

mk_rews: automatically includes strip_shyps, zero_var_indexes;

New file for theorems of Porder0 Dervie the prperties of partial orders from the axiomatic type class po

tuned comments;

Examples are adopted to the changes from HOLCF. Classlib is reduced. Classlib still uses arities, Classlib will change completely to new classes of ADTs

using types one = unit lift and translations causes troubles between the type one and the constant one. The later was changed to ONE

Changes of HOLCF from Oscar Slotosch: 1. axclass instead of class * less instead of less_fun, less_cfun, less_sprod, less_cprod, less_ssum, less_up, less_lift * @x.!y.x<<y instead of UUU instead of UU_fun, UU_cfun, ... * no witness type void needed (eliminated Void.thy.Void.ML) * inst_<typ>_<class> derived as theorems 2. improved some proves on less_sprod and less_cprod * eliminated the following theorems Sprod1.ML: less_sprod1a Sprod1.ML: less_sprod1b Sprod1.ML: less_sprod2a Sprod1.ML: less_sprod2b Sprod1.ML: less_sprod2c Sprod2.ML: less_sprod3a Sprod2.ML: less_sprod3b Sprod2.ML: less_sprod4b Sprod2.ML: less_sprod4c Sprod3.ML: less_sprod5b Sprod3.ML: less_sprod5c Cprod1.ML: less_cprod1b Cprod1.ML: less_cprod2a Cprod1.ML: less_cprod2b Cprod1.ML: less_cprod2c Cprod2.ML: less_cprod3a Cprod2.ML: less_cprod3b 3. new classes: * cpo<po, * chfin<pcpo, * flat<pcpo, * derived: flat<chfin to do: show instances for lift 4. Data Type One * Used lift for the definition: one = unit lift * Changed the constant one into ONE 5. Data Type Tr * Used lift for the definition: tr = bool lift * adopted definitions of if,andalso,orelse,neg * only one theory Tr.thy,Tr.ML instead of Tr1.thy,Tr1.ML, Tr2.thy,Tr2.ML * reintroduced ceils for =TT,=FF 6. typedef * Using typedef instead of faking type definitions to do: change fapp, fabs from Cfun1 to Rep_Cfun, Abs_Cfun 7. adopted examples and domain construct to theses changes These changes eliminated all rules and arities from HOLCF

*** empty log message ***

reflecting my recent changes of the classical reasoner

reflecting my recent changes of the simplifier and classical reasoner

added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss, safe_asm_more_full_simp_ta, clasimpset HOL_css with modification functions new addss (old version retained as unsafe_addss), new Addss (old version retained as Unsafe_Addss), new auto_tac (old version retained as unsafe_auto_tac),

cosmetic

updated mini_ss