improved eq_sg; cosmetical change in print_sg;

added eq_set;

correction to cut tactics

no longer removes *.z

now makes HOLCF

added strs, big_list, writeln;

added simple_string_of_typ, simple_pprint_typ; various internal changes;

added type 'syntax'; added syntax_consts (_K, _explode, _implode, ...);

minor internal changes;

syntax for type abbreviations;

(this is a preliminary release) type abbreviations;

added if_none, parents, commas, gen_duplicates, duplicates, assoc2; changed cat_lines: no final "\n";

replaced pprint_sg by Sign.pprint_sg; added Syntax.simple_pprint_typ;

replaced eq_sg by Sign.eq_sg;

removed eq_sg, pprint_sg, print_sg (now in sign.ML); removed cterm_fun, read_ctyp (now in thm.ML); print_theory: now shows all contents;

major cleanup; added eq_sig; added print_sg (full contents), pprint_sg (stamps only); added certify_typ, certify_term; changed read_typ: result now certified;

extend_theory: changed type of "abbrs" arg; added cterm_fun, read_ctyp (from drule.ML); ctyp_of, cterm_of, etc.: now use Sign.certify_...; assumption: now uses Envir.is_empty; bicompose_aux: fixed BUG (unifier with empty "asol" but non-empty "iTs" wasn't applied); fixed axioms_of;

made error message "file not found" more informative

case was renamed to sum_case

added is_empty: env -> bool, minidx: env -> int option;

added HOLCF

removed square and fact

HOLCF examples

Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.

commented out sig constraint of functor (for debugging purposes);

changed SYNTAX_FILES;

contains remaining parts of xgram.ML and extension.ML; syn_ext replaces xgram and ext;

minor internal changes;

MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables now much leaner (eliminated gramgraph, all data except tables of old parser are shared); simplified the internal interfaces for syntax extension; added translations for _explode, _implode (experimental);

MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables now much leaner (eliminated gramgraph, all data except tables of old parser are shared); simplified the internal interfaces for syntax extension;

added some utils: commas, breaks, fbreaks, block, parents, list, str_list;

cosmetic changes;

minor cleanup; added extend, merge; added {lookup,make,dest}_multi;

major cleanup and reorganisation; added generic_extend, generic_merge; added various minor functions;

corrected comment

Updated refs to old Sign functions

Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g

Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field of a theorem to be regarded as a cterm -- avoids expensive calls to cterm_of.

some optimizations of Larry's

corrected comments

corrected comments

optimized net for matching of abstractions to speed up simplifier

moved misplaced comment

removed Syntax/parse_tree.ML;

optimized the number of eta-contractions in rewriting

added a check for existence of a temporary file before removing it

used unlink for delete_files instead of calling rm

commented out sig constraint of functor (for debugging purposes);

ZF/perm/image_comp: new

got rid of METAHYPS due to the change of the basic simplification routines (see update of Pure/{thm,drule,tactic}.ML)

adapted a proof to the new solver (see change of FOL/simpdata.ML)

updated solver of FOL_ss. see change of HOL/simpdata.ML

added new parameter to the simplification tactics which indicates if assumptions are to be simplified and/or to be used when simplifying the conclusion. This gets rid of METAHYPS and speeds up simplification of goals with big assumptions.

added lexical class of type variables

shortened msg

added fake_cterm_of to speed up rewriting

commented out sig constraint of functor (for debugging purposes);

changed tracing of simplifier

optimized simplifier - signature of rewritten term stays constant

added "Reading thy-File" message

added subsig: sg * sg -> bool to test if one signature is contained in another.

added sys_error;

fixed a bug in update/next_level which occured when a child wasn't loaded

added empty type-abbr field to extend_theory

added []-field to extend_theory: no type abbreviations.

Added []-field to extend_theory to accomodate type abbreviations.

Necessary changes to accomodate type abbreviations.

pretty_thm is now exported;

new section for equality properties

Updated read_insts to approximate simultaneous type checking of substitution pairs.

added isabelle-users paragraph

added mention of simplifier, splitter, hypsubst

new year

updated instantiate to deal with type clashes

ZF/equalities/SUM_eq_UN: new ZF/equalities: corrected bound variable anomalies in some distributive laws

Pure/tactic/compose_inst_tac: when catching exception THM, prints the message before failing!! This reports the reason for failure in cases like by (res_inst_tac [("P", "?Q(a)")] mp 1); in which ?Q appears in mp with a different type.

deleted harmful basify, which pulled rewrite rules down to base type. Not needed for new simplifier.

added rep_tsig

last minute changes, eg literal tokens -> delimiters and valued tokens -> names.

ZF/univ/in_Vfrom_limit: new ZF/univ/sum_in_Vfrom, etc: streamlined proofs using in_Vfrom_limit

ZF/ord/Ord_Un,Ord_Int,Un_upper1_le,Un_upper2_le: new

Typos and style

Changed Acknowledgements

Acknowledged Carsten Clasohm

New distributive laws for Sigma and UN

removal of amssymbols.sty and lcp.sty; addition of iman.sty

ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted them, to make the most of the load-path mechanism. (use_thy adds the new theory to the list of loaded theories.)

minor corrections

new references

now inspects FOLP_build_completed

now declares FOLP_build_completed

*** empty log message ***

*** empty log message ***

ZF/ex/llist_eq/lleq_Int_Vset_subset_lemma, ZF/ex/counit/counit2_Int_Vset_subset_lemma: now uses QPair_Int_Vset_subset_UN ZF/ex/llistfn/flip_llist_quniv_lemma: now uses transfinite induction and QPair_Int_Vset_subset_UN ZF/ex/llist/llist_quniv_lemma: now uses transfinite induction and QPair_Int_Vset_subset_UN

changed split_filename, remove_ext; added base_name;

*** empty log message ***

ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many coinduction proofs ZF/quniv: deleted the following obsolete theorems (saved on Isa/old): Int_Vfrom_0_in_quniv Pair_in_quniv_D QInl_Int_Vfrom_succ_in_quniv QInl_Int_quniv_in_quniv QPair_Int_Vfrom_in_quniv QPair_Int_Vfrom_succ_in_quniv QPair_Int_quniv_eq QPair_Int_quniv_in_quniv QPair_Int_quniv_in_quniv product_Int_quniv_eq quniv_Int_Vfrom zero_Int_in_quniv

extend: cleaned up, adapted for new Syntax.extend; extend, merge: improved roots (logical_types) handling;

*** empty log message ***

added (partial) extend_tables; improved extend; fixed roots handling of extend and merge;

changed datatype ext;

improved comments;

added SCANNER; changed scan_any: no longer uses take_prefix;

added Scanner;

added logical_types

improved comments;

added equal, not_equal: ''a -> ''a -> bool

Minor edits to discussion of use_thy

Correction to eta-contraction; thanks to Markus W.

Correction to page 16; thanks to Markus W.

Corrected errors found by Marcus Wenzel.

changed some names and deleted *NORMALIZED*

corrected obvious errors;

corrected obvious errors;

*** empty log message ***

corrected some obvious errors;

changed beginning of "Reading a new theory", added index "automatic loading"

corrected trivial typo;

corrected trivial typo;

fixed a bug in get_filenames, changed output of use_thy