kleing [Fri, 22 Apr 2005 00:31:30 +0200] rev 15806
test stable and devel version of smlnj
wenzelm [Thu, 21 Apr 2005 22:10:12 +0200] rev 15805
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm [Thu, 21 Apr 2005 22:06:18 +0200] rev 15804
The CPure theory -- Pure with alternative application syntax.
wenzelm [Thu, 21 Apr 2005 22:06:00 +0200] rev 15803
The Pure theory.
wenzelm [Thu, 21 Apr 2005 22:04:01 +0200] rev 15802
removed;
wenzelm [Thu, 21 Apr 2005 22:02:06 +0200] rev 15801
superceded by Pure.thy and CPure.thy;
wenzelm [Thu, 21 Apr 2005 22:00:28 +0200] rev 15800
adapt theories and ML files to new CPure/Pure arrangement;
berghofe [Thu, 21 Apr 2005 19:16:19 +0200] rev 15799
Adapted use command to new behaviour of Toplevel.node_trans
berghofe [Thu, 21 Apr 2005 19:13:03 +0200] rev 15798
Adapted to new interface of instantiation and unification / matching functions.
berghofe [Thu, 21 Apr 2005 19:12:03 +0200] rev 15797
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.