1993-12-01 lcp 1993-12-01 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.)
1993-12-01 lcp 1993-12-01 minor corrections
1993-12-01 lcp 1993-12-01 new references
1993-12-01 lcp 1993-12-01 now inspects FOLP_build_completed
1993-12-01 lcp 1993-12-01 now declares FOLP_build_completed
1993-11-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-30 lcp 1993-11-30 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
1993-11-30 wenzelm 1993-11-30 changed split_filename, remove_ext; added base_name;
1993-11-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-30 lcp 1993-11-30 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
1993-11-29 wenzelm 1993-11-29 extend: cleaned up, adapted for new Syntax.extend; extend, merge: improved roots (logical_types) handling;
1993-11-29 wenzelm 1993-11-29 *** empty log message ***
1993-11-29 wenzelm 1993-11-29 added (partial) extend_tables; improved extend; fixed roots handling of extend and merge;
1993-11-29 wenzelm 1993-11-29 changed datatype ext;
1993-11-29 wenzelm 1993-11-29 improved comments;
1993-11-29 wenzelm 1993-11-29 added SCANNER; changed scan_any: no longer uses take_prefix;
1993-11-29 wenzelm 1993-11-29 added Scanner;
1993-11-29 nipkow 1993-11-29 added logical_types
1993-11-29 wenzelm 1993-11-29 improved comments;
1993-11-29 wenzelm 1993-11-29 added equal, not_equal: ''a -> ''a -> bool
1993-11-26 lcp 1993-11-26 Minor edits to discussion of use_thy
1993-11-26 lcp 1993-11-26 Correction to eta-contraction; thanks to Markus W.
1993-11-26 lcp 1993-11-26 Correction to page 16; thanks to Markus W.
1993-11-26 lcp 1993-11-26 Corrected errors found by Marcus Wenzel.
1993-11-25 nipkow 1993-11-25 changed some names and deleted *NORMALIZED*
1993-11-25 wenzelm 1993-11-25 corrected obvious errors;
1993-11-25 wenzelm 1993-11-25 corrected obvious errors;
1993-11-25 wenzelm 1993-11-25 *** empty log message ***
1993-11-25 wenzelm 1993-11-25 corrected some obvious errors;
1993-11-25 clasohm 1993-11-25 changed beginning of "Reading a new theory", added index "automatic loading"
1993-11-25 wenzelm 1993-11-25 corrected trivial typo;
1993-11-25 wenzelm 1993-11-25 corrected trivial typo;
1993-11-25 clasohm 1993-11-25 fixed a bug in get_filenames, changed output of use_thy
1993-11-25 nipkow 1993-11-25 asm_full_simp_tac now fails if there are no subgoals
1993-11-25 wenzelm 1993-11-25 added subsection 'Classes and types'; added syntax and short explanation of translations section;
1993-11-25 wenzelm 1993-11-25 added Syntax.read_typ; Syntax.extend: added read_ty, removed def_sort argument;
1993-11-25 wenzelm 1993-11-25 Sign.extend: Syntax.extend now called with read_ty;
1993-11-25 wenzelm 1993-11-25 removed section 'Classes and types';
1993-11-25 clasohm 1993-11-25 added index commands, removed last paragraph of "Using Poly/ML"
1993-11-23 nipkow 1993-11-23 changed itmath trickery to be compatible with NFSS (itmath.sty)
1993-11-22 nipkow 1993-11-22 minor changes
1993-11-22 clasohm 1993-11-22 added chapter "Defining Theories" and made changes for new Readthy functions
1993-11-22 wenzelm 1993-11-22 *** empty log message ***
1993-11-22 wenzelm 1993-11-22 *** empty log message ***
1993-11-22 wenzelm 1993-11-22 various minor changes;
1993-11-22 nipkow 1993-11-22 Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
1993-11-19 lcp 1993-11-19 Reformatting of SIMPLIFIER figure
1993-11-19 lcp 1993-11-19 Trivial spacing corrections
1993-11-19 lcp 1993-11-19 Documents not, and, or, xor: boolean ops
1993-11-19 lcp 1993-11-19 Many edits suggested by Grundy & Thompson
1993-11-19 lcp 1993-11-19 expandshort and other trivial changes
1993-11-18 lcp 1993-11-18 expandshort
1993-11-18 lcp 1993-11-18 Misc modifs such as expandshort
1993-11-16 clasohm 1993-11-16 added loaded_thys to signature and removed list_/set_loaded
1993-11-16 clasohm 1993-11-16 changed use_thy's parameter to exact theory name
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files
1993-11-16 clasohm 1993-11-16 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
1993-11-16 clasohm 1993-11-16 replaced \un by \union in "Simplification sets"
1993-11-16 clasohm 1993-11-16 changed use_thy's parameter to exact theory name