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;

added thy_data; misc fixes;

use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML;

adapted to new implicit simpset;

adapted to new implicit claset;

fixed thy dependencies;

aded thy_data;

HOL theory data.

added thy_data.ML;

new implicit simpset mechanism based on Sign.sg anytype data;

new implicit claset mechanism based on Sign.sg anytype data; tuned warnings;

adapted to new implicit claset mechanism;

fix references to implicit claset and simpset;

do not overwrite backup files;

set_session renamed to add_session;

tuned error msg;

made SML/97 happy;

expand_option_bind -> split_option_bind

expand_option_case -> split_option_case

*** empty log message ***

expand_list_case -> split_list_case

Indexed split_t_case.

Documented `split_t_case' thm genearted by datatype.

Fixed comments

New treatment of overloading\!

New syntax function for types

Faster lexing

New way of referring to Basis Library

mended type constraint\!

Set.thy was too specific

New Blast_tac (and minor tidying...)

Auto update

propagate exn msg;

dup sections: warning instead of error;

Session, Context;

tuned;

added mixfix_args;

*** empty log message ***

added str_of_sg: sg -> string; improved error handling of data access;

added mixfix_args;

tuned thy_data;

tuned init_data;

added thy_data;