1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-15 clasohm 1996-02-15 updated documentation of MAKE_HTML
1996-02-15 nipkow 1996-02-15 Added a few thms and the new theory RelPow.
1996-02-13 nipkow 1996-02-13 Added check for duplicate vars with distinct types/sorts (nodup_Vars)
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