src/HOL/Subst/Setplus.thy
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1476 608483c2122a
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML

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