Subst/Setplus.thy
author clasohm
Wed, 02 Mar 1994 12:26:55 +0100
changeset 48 21291189b51e
parent 0 7949f97df77a
permissions -rw-r--r--
changed "." to "$" and Cons to infix "#" to eliminate ambiguity

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