1996-02-13 nipkow 1996-02-13 added nodup_Vars check in cterm_of. Prevents same var with distinct types.
1996-02-13 clasohm 1996-02-13 added dest_comb, dest_abs and mk_prop for manipulating cterms
1996-02-13 clasohm 1996-02-13 cond_timeit now uses totalCPUTimer instead of starting new ones every time it is invoked; hopefully this will fix the strange SML109 bug
1996-02-10 clasohm 1996-02-10 make_html now only remains set if MAKE_HTML=true
1996-02-09 nipkow 1996-02-09 More examples.
1996-02-09 nipkow 1996-02-09 Small changes.
1996-02-09 nipkow 1996-02-09 Added typevarlist
1996-02-09 nipkow 1996-02-09 replace sstac
1996-02-09 nipkow 1996-02-09 Introduced qed_spec_mp.
1996-02-09 nipkow 1996-02-09 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
1996-02-09 clasohm 1996-02-09 renamed expand_typ to norm_typ
1996-02-08 clasohm 1996-02-08 simplified bind_thm
1996-02-07 clasohm 1996-02-07 new SML heap images are now removed
1996-02-07 nipkow 1996-02-07 Modified datatype com. Added (part of) relative completeness proof for Hoare logic.
1996-02-06 clasohm 1996-02-06 made Isabelle compatible with SML/NJ 1.09
1996-02-06 clasohm 1996-02-06 expanded tabs
1996-02-06 clasohm 1996-02-06 expanded tabs
1996-02-05 clasohm 1996-02-05 expanded tabs
1996-02-05 clasohm 1996-02-05 expanded tabs; incorporated Konrad's changes
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1996-02-05 clasohm 1996-02-05 expanded tabs
1996-02-05 clasohm 1996-02-05 expanded tabs
1996-02-02 clasohm 1996-02-02 renamed subtype.ML to typedef.ML
1996-02-01 nipkow 1996-02-01 documented split_all_tac in HOL.
1996-02-01 clasohm 1996-02-01 renamed subtype.ML to typedef.ML
1996-02-01 clasohm 1996-02-01 fixed two little bugs
1996-01-31 nipkow 1996-01-31 right-hard -> right-hand
1996-01-31 nipkow 1996-01-31 Typo
1996-01-30 clasohm 1996-01-30 fixed typo
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-30 clasohm 1996-01-30 expanded tabs; removed commit() from ROOT.ML
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-30 clasohm 1996-01-30 fixed typo
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 expanded tabs
1996-01-29 clasohm 1996-01-29 removed tabs
1996-01-29 clasohm 1996-01-29 added facility to associate arbitrary data with theories
1996-01-29 clasohm 1996-01-29 added absolute_path
1996-01-29 clasohm 1996-01-29 changed the way simpsets and information about datatypes are stored
1996-01-26 nipkow 1996-01-26 Streamlined defs in Relation and added new intro/elim rules to do with pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...
1996-01-26 clasohm 1996-01-26 extended warning regarding MAKE_HTML databases
1996-01-26 clasohm 1996-01-26 added warning for databases made with set MAKE_HTML
1996-01-23 nipkow 1996-01-23 Added vcwp
1996-01-23 paulson 1996-01-23 Renamed letI to LetI (for consistency)
1996-01-23 paulson 1996-01-23 Added discussion of "let" and pattern-matching
1996-01-23 paulson 1996-01-23 Stylistic changes to discussion of pattern-matching
1996-01-23 nipkow 1996-01-23 Added a verified verification-condition generator.
1996-01-20 paulson 1996-01-20 Ran expandshort
1996-01-19 paulson 1996-01-19 Now expands TABS as well
1996-01-18 paulson 1996-01-18 trivial updates Isabelle94-5
1996-01-18 paulson 1996-01-18 New version number
1996-01-15 wenzelm 1996-01-15 *** empty log message ***
1996-01-15 wenzelm 1996-01-15 added Lattice demo;
1996-01-15 wenzelm 1996-01-15 added this stuff;
1996-01-15 wenzelm 1996-01-15 improved printing of errors in 'defs'; fixed small bug in 'standard' (it used to fail stripping shyps in some cases);
1996-01-15 clasohm 1996-01-15 added comments
1996-01-15 clasohm 1996-01-15 beautified file_info a bit
1996-01-15 clasohm 1996-01-15 fixed bug in file_info
1996-01-11 nipkow 1996-01-11 Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.