Each datatype t now proves a theorem split_t_case_prem P(t_case f1 ... fn x) = (~((? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) | ... (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn)) ) )

Perl no longer optional;

deriv: eliminated references to theory;

tuned;

tuned;

hyp_subst_tac checks if the equality has type variables and uses a suitable method if so. Affects the dest_eq function

subgoal_tac displays a warning if the new subgoal has type variables

mkdir -p bin;

Tools/8bit: ./mk;

*** empty log message ***

tuned;

abandoned generation of tmp files

various improvements

reflecting changes of isa2latex

several minor improvements

added ax2isa

added ax2isa

added isabelle14 and isabelle24

removed gererated files

added entry for manual

*** empty log message ***

Now introduces Safe_tac

Ran expandshort, especially to introduce Safe_tac

Adapted to removal of UN1_I, etc

Adapted to removal of UN1_I, etc

UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves

Expandshort; new theorem le_square

generalized UNION1 to UNION

Tidied Key_supply3

fixed comment

UNIV & UNION1

Ran expandshort, especially to introduce Safe_tac

Ran expandshort, especially to introduce Safe_tac

adapted typed_print_translation;

tuned record_info;

fixed exception OPTION;

adapted pure_trfunsT; added type_tr/tr'; eliminated mk_ofclassS_tr';

print translation: added show_sorts argument;

adapted syn_ext_trfunsT;

adapted extend_trfunsT;

fixed exception OPTION;

added TYPE syntax; tuned;

fixed exception OPTION;

adapted add_trfunsT; defs: admit TYPE arguments;

adapted add_trfunsT;

fixed exception OPTION; added try, can;

base root = "";

Added an alternativ version of AutoChopper and a theory for the conversion of automata into regular sets.

removed redundant ball_image added image_cong and not_empty added ball and bex of UNIV

removed redundant ball_empty and bex_empty (see equalities.ML)

added several theorems

added the, option_map, and case analysis theorems

added zip and nodup

added theorems for Eps

tuned usage;

HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;

tuned to make non-Poly/MLs happy;

tuned 'records' stuff;

added pretty_ctyp;

tuned;

type object = exn (enhance readability);

*** empty log message ***

* removed "axioms" and "generated by" section * replaced "ops" section by extended "consts" section, which is capable of handling the continuous function space "->" directly * domain package: now uses normal mixfix annotations (instead of cinfix...)

simplified (and corrected) syntax definition of fapp

data kinds 'datatypes', data kinds 'records' added

removed old datatype_info;

added Thy/path.ML;

Logic.loops -> Logic.rewrite_rule_ok

logic: loops -> rewrite_rule_ok added rewrite_rule_extra_vars thm: Rewrite rules must not introduce new type vars on rhs. This lead to an incompleteness, is now banned, and the code has been simplified.

added path.ML;

added base; tuned;

Abstract algebra of file paths. External representation Unix-style.

tuned;

removed old thy data stuff;

fixed set_current_thy pattern;

isatool fixclasimp;

isatool fixclasimp;

adapted to new datatypes thy info;

tuned;

datatypes;

nat datatype_info moved to Nat.thy;

added MLtext section;

added distinct_fst_string;

tuned: distinct_fst_string;

isatool fixclasimp;

export const_decls parser;

isatool fixclasimp;

CLASET';

moved cladata.ML, simpdata.ML to ROOT.ML;

adapted to new implicit claset;

adapted to new implicit simpset;

added claset thy_data;

added simpset thy_data;

isatool fixclasimp;

isatool fixclasimp; removed several blast_tacs;

isatool fixclasimp;