diff -r 000000000000 -r 7949f97df77a Subst/setplus.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Subst/setplus.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,14 @@
+(*  Title: 	Substitutions/setplus.thy
+    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Minor additions to HOL's set theory
+*)
+
+Setplus = Set + 
+
+rules
+
+  ssubset_def    "A < B == A <= B & ~ A=B"
+
+end