Subst/setplus.thy
author clasohm
Wed, 02 Nov 1994 15:26:13 +0100
changeset 157 45d0cf6e309d
parent 0 7949f97df77a
permissions -rw-r--r--
added IOA files

(*  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