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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 968
diff changeset
     1
(*  Title:      Substitutions/setplus.thy
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 968
diff changeset
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
968
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
     4
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
     5
Minor additions to HOL's set theory
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
     6
*)
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
     7
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
     8
Setplus = Set + 
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
     9
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
    10
rules
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
    11
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
    12
  ssubset_def    "A < B == A <= B & ~ A=B"
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
    13
3cdaa8724175 converted Subst with curried function application
clasohm
parents:
diff changeset
    14
end