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

asm_full_simp_tac now fails if there are no subgoals

added subsection 'Classes and types'; added syntax and short explanation of translations section;

added Syntax.read_typ; Syntax.extend: added read_ty, removed def_sort argument;

Sign.extend: Syntax.extend now called with read_ty;

removed section 'Classes and types';

added index commands, removed last paragraph of "Using Poly/ML"

changed itmath trickery to be compatible with NFSS (itmath.sty)

minor changes

added chapter "Defining Theories" and made changes for new Readthy functions

*** empty log message ***

*** empty log message ***

various minor changes;

Fixed bug in rewriter (fun impc) discovered by Marcus Moore.

Reformatting of SIMPLIFIER figure

Trivial spacing corrections

Documents not, and, or, xor: boolean ops

Many edits suggested by Grundy & Thompson

expandshort and other trivial changes

expandshort

Misc modifs such as expandshort

added loaded_thys to signature and removed list_/set_loaded

changed use_thy's parameter to exact theory name

made pseudo theories for all ML files; documented dependencies between all thy and ML files

moved call of store_theory to end of use t.thy; use t.ML; use_thy now needs the exact theory name (capital/lower letters); improved handling of incompletly read theories; added function unlink_thy, removed function relations; added reference variable delete_tmpfile; removed some bugs

replaced \un by \union in "Simplification sets"

changed use_thy's parameter to exact theory name

changed all co- and co_ to co ZF/ex/llistfn: new coinduction example: flip ZF/ex/llist_eq: now uses standard pairs not qpairs

boolE: changed to have equality assumptions instead of P(c); proved many boolean laws

Added commentary

fun parents: removed pp block (didn't have any effect)

changed application format for pretty-printer

Misc updates

Misc updates

changed formatting for application

Changed the simplifier: if the subgoaler proves an unexpected thm, chances are, it is an instance of the expected thm. Instead of aborting, rewriting now fails at that point.

Various updates for Isabelle-93

new style file

adapted "Defining theories" to new use_thy

replaced by current version;

replaced by current version;

*** empty log message ***

Initial revision

Initial revision

Initial revision

Target "test" now depends on examples files

Target "test" now depends on examples files

fixed a bug in POLY.ML: delete_file didn't close streams; added function pwd to get current working directory

renamed hard-quant.ML to hardquant.ML

renamed int-prover.ML to intprover.ML, used exact theory names for use_thy

renamed int-prover.ML to intprover.ML, used exact theory names in ROOT.ML

now forbids semicolons in the body of br, etc. No longer requires it to end the line.

Minor changes; addition of counit.ML

change of my address

Added documenation of change_simp.

renamed co_inductive.ML to coinductive.ML

renamed twos-compl.ML to twos_compl.ML

renamed some files

commented out install_pp for term, typ

added infix delsimps

added function del_simps

deletion of obsolete/private files; update of README

minor changes e.g. datatype_elims

now uses datatype_intrs and datatype_elims

updated version to October 93

no longer specifies "-h 15000". Instead $ISABELLECOMP should include any switch settings.

corrected some spelling mistakes; removed a bug that made it impossible to read theories that don't have a ML file; extended syntax for bases in syntax.ML: a string can be used to specify a theory that is to be read but is not merged into the base (useful for pseudo theories used to document the dependencies of ML files)

added white-space; made ~: a fake infix;