# HG changeset patch
# User paulson
# Date 910960023 -3600
# Node ID 36b5559d822494be5cc86cb7529a466b3fe55d4c
# Parent  4d7320490be4f17ddbaf4a973aef084ca255f9ab
no longer loads Fun so that the Fun proofs can use equalities.thy

diff -r 4d7320490be4 -r 36b5559d8224 src/HOL/subset.thy
--- a/src/HOL/subset.thy	Fri Nov 13 13:26:16 1998 +0100
+++ b/src/HOL/subset.thy	Fri Nov 13 13:27:03 1998 +0100
@@ -4,4 +4,4 @@
     Copyright   1994  University of Cambridge
 *)
 
-subset = Fun
+subset = Set