wenzelm [Thu, 03 Feb 1994 13:53:08 +0100] rev 250
extend_theory: changed type of "abbrs" arg;
added cterm_fun, read_ctyp (from drule.ML);
ctyp_of, cterm_of, etc.: now use Sign.certify_...;
assumption: now uses Envir.is_empty;
bicompose_aux: fixed BUG (unifier with empty "asol" but non-empty "iTs"
wasn't applied);
fixed axioms_of;
clasohm [Wed, 02 Feb 1994 11:15:22 +0100] rev 249
made error message "file not found" more informative
nipkow [Wed, 26 Jan 1994 22:07:06 +0100] rev 248
case was renamed to sum_case
wenzelm [Mon, 24 Jan 1994 12:03:53 +0100] rev 247
added is_empty: env -> bool, minidx: env -> int option;
nipkow [Thu, 20 Jan 1994 13:35:40 +0100] rev 246
added HOLCF
nipkow [Thu, 20 Jan 1994 12:38:02 +0100] rev 245
removed square and fact
nipkow [Wed, 19 Jan 1994 17:40:26 +0100] rev 244
HOLCF examples
nipkow [Wed, 19 Jan 1994 17:35:01 +0100] rev 243
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
wenzelm [Wed, 19 Jan 1994 14:45:07 +0100] rev 242
commented out sig constraint of functor (for debugging purposes);
wenzelm [Wed, 19 Jan 1994 14:28:35 +0100] rev 241
changed SYNTAX_FILES;