changeset 3192 | a75558a4ed37 |
parent 3191 | 14bd6e5985f1 |
child 3193 | fafc7e815b70 |
--- a/src/HOL/Subst/Setplus.thy Thu May 15 12:29:59 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* 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