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
1993-11-15 lcp 1993-11-15 changed all co- and co_ to co ZF/ex/llistfn: new coinduction example: flip ZF/ex/llist_eq: now uses standard pairs not qpairs
1993-11-15 lcp 1993-11-15 boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
1993-11-15 lcp 1993-11-15 Added commentary
1993-11-15 wenzelm 1993-11-15 fun parents: removed pp block (didn't have any effect)
1993-11-14 nipkow 1993-11-14 changed application format for pretty-printer
1993-11-12 lcp 1993-11-12 Misc updates
1993-11-12 lcp 1993-11-12 Misc updates
1993-11-11 nipkow 1993-11-11 changed formatting for application
1993-11-11 nipkow 1993-11-11 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.
1993-11-11 lcp 1993-11-11 Various updates for Isabelle-93
1993-11-11 lcp 1993-11-11 new style file
1993-11-11 clasohm 1993-11-11 adapted "Defining theories" to new use_thy
1993-11-11 wenzelm 1993-11-11 replaced by current version;
1993-11-11 wenzelm 1993-11-11 replaced by current version;
1993-11-11 wenzelm 1993-11-11 *** empty log message ***
1993-11-10 lcp 1993-11-10 Initial revision
1993-11-10 lcp 1993-11-10 Initial revision
1993-11-09 lcp 1993-11-09 Initial revision
1993-11-09 lcp 1993-11-09 Target "test" now depends on examples files
1993-11-09 lcp 1993-11-09 Target "test" now depends on examples files
1993-11-09 clasohm 1993-11-09 fixed a bug in POLY.ML: delete_file didn't close streams; added function pwd to get current working directory
1993-11-09 clasohm 1993-11-09 renamed hard-quant.ML to hardquant.ML
1993-11-09 clasohm 1993-11-09 renamed int-prover.ML to intprover.ML, used exact theory names for use_thy
1993-11-09 clasohm 1993-11-09 renamed int-prover.ML to intprover.ML, used exact theory names in ROOT.ML
1993-11-09 lcp 1993-11-09 now forbids semicolons in the body of br, etc. No longer requires it to end the line.
1993-11-08 lcp 1993-11-08 Minor changes; addition of counit.ML
1993-11-05 nipkow 1993-11-05 change of my address
1993-11-05 lcp 1993-11-05 Added documenation of change_simp.
1993-11-04 clasohm 1993-11-04 renamed co_inductive.ML to coinductive.ML
1993-11-04 clasohm 1993-11-04 renamed twos-compl.ML to twos_compl.ML
1993-11-04 clasohm 1993-11-04 renamed some files
1993-11-04 wenzelm 1993-11-04 commented out install_pp for term, typ
1993-10-29 nipkow 1993-10-29 added infix delsimps
1993-10-29 nipkow 1993-10-29 added function del_simps
1993-10-28 lcp 1993-10-28 deletion of obsolete/private files; update of README
1993-10-28 lcp 1993-10-28 minor changes e.g. datatype_elims
1993-10-28 lcp 1993-10-28 now uses datatype_intrs and datatype_elims
1993-10-28 lcp 1993-10-28 updated version to October 93
1993-10-27 lcp 1993-10-27 no longer specifies "-h 15000". Instead $ISABELLECOMP should include any switch settings.
1993-10-26 clasohm 1993-10-26 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)
1993-10-25 wenzelm 1993-10-25 added white-space; made ~: a fake infix;
1993-10-25 wenzelm 1993-10-25 added white-space; made ~= a fake infix;
1993-10-22 clasohm 1993-10-22 removed a bug that occured when a path was specified for use_thy's parameter and the theory was created in a .ML file
1993-10-22 lcp 1993-10-22 ZF/ex/tf,tf_fn: renamed the variable tf to f everywhere
1993-10-22 clasohm 1993-10-22 renamed some files
1993-10-22 clasohm 1993-10-22 added -h 15000 for Poly/ML in Makefile, changed ROOT.ML for new Readthy
1993-10-22 clasohm 1993-10-22 changes in Readthy: - reads needed base theories automatically - keeps a time stamp for all read files - update function - checks for cycles - path list that is searched for files - reads theories that are created in .ML files - etc.
1993-10-22 clasohm 1993-10-22 delete_file now has type string -> unit in both NJ and POLY, use of Pure/Thy/ROOT has been moved to the end of Pure/ROOT again
1993-10-22 clasohm 1993-10-22 changes for new Readthy
1993-10-22 lcp 1993-10-22 sample datatype defs now use datatype_intrs, datatype_elims
1993-10-22 lcp 1993-10-22 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works ZF/intr-elim/elim_rls: applied make_elim to succ_inject! ZF/fin: changed type_intrs in inductive def ZF/datatype/datatype_intrs, datatype_elims: renamed from data_typechecks, data_elims ZF/list: now uses datatype_intrs
1993-10-22 lcp 1993-10-22 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the right sides of the defs
1993-10-22 lcp 1993-10-22 goals/print_top,prepare_proof: now call \!print_goals_ref