1997-04-24 nipkow 1997-04-24 Updates because nat_ind_tac no longer appends "1" to the ind.var.
1996-12-18 oheimb 1996-12-18 The previous log message was wrong. The correct one is: generalized handling of type expressions, type variables and sorts
1996-12-18 oheimb 1996-12-18 removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
1996-11-29 oheimb 1996-11-29 modified file headers renamed lift to fup
1996-11-28 paulson 1996-11-28 Replaced map...~~ by Tried to tidy up the indenting...
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-06-27 oheimb 1996-06-27 re-added when_funs to library.ML
1996-06-26 oheimb 1996-06-26 function names in when_rews now meta-quantified
1996-05-31 oheimb 1996-05-31 adapted use of monofun_cfun_arg
1996-04-23 oheimb 1996-04-23 *** empty log message ***
1996-04-04 oheimb 1996-04-04 Removed 8bit characters used by mistake
1996-04-03 oheimb 1996-04-03 *** empty log message ***
1996-04-03 oheimb 1996-04-03 Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
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-01-30 clasohm 1996-01-30 expanded tabs
1995-10-06 regensbu 1995-10-06 added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb