wenzelm [Thu, 22 Oct 1998 12:32:42 +0200] rev 5727
fixed index.html;
wenzelm [Thu, 22 Oct 1998 12:26:55 +0200] rev 5726
tuned;
record package;
wenzelm [Thu, 22 Oct 1998 11:09:43 +0200] rev 5725
tuned;
paulson [Thu, 22 Oct 1998 10:58:50 +0200] rev 5724
standard Blast_tac demos
paulson [Thu, 22 Oct 1998 10:58:18 +0200] rev 5723
tidying
paulson [Thu, 22 Oct 1998 10:57:18 +0200] rev 5722
locales
berghofe [Wed, 21 Oct 1998 17:57:02 +0200] rev 5721
Changed interface of inductive.
berghofe [Wed, 21 Oct 1998 17:55:18 +0200] rev 5720
Changed interface of rep_datatype: Characteristic theorems
of datatypes are now specified by xstrings.
berghofe [Wed, 21 Oct 1998 17:53:16 +0200] rev 5719
Changed interface.
berghofe [Wed, 21 Oct 1998 17:52:38 +0200] rev 5718
Changed interface of add_inductive: monos and con_defs are now
lists of xstrings.
berghofe [Wed, 21 Oct 1998 17:48:02 +0200] rev 5717
Changed syntax of inductive.
berghofe [Wed, 21 Oct 1998 17:46:00 +0200] rev 5716
Changed syntax of rep_datatype and inductive: Theorems
are no longer specified by a string of ML type "thm list" but
by a comma-separated list of identifiers, which are looked
up in the theory.
berghofe [Wed, 21 Oct 1998 17:40:35 +0200] rev 5715
Added theorem prod_induct (needed for rep_datatype).
berghofe [Wed, 21 Oct 1998 17:38:47 +0200] rev 5714
Changed syntax of rep_datatype.