isabelle: src/HOL/Subst/Setplus.thy@836950047d85 (annotated)

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

author	paulson
	Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868	836950047d85
parent 1476	608483c2122a
permissions	-rw-r--r--