# HG changeset patch
# User wenzelm
# Date 939066409 -7200
# Node ID 222b715b5d24881d054f62d53c9c2ffaec0344ff
# Parent  9a6783fdb9a5d28b70d756011ecd2a17a8a8ff9c
Tools/typedef_package.ML;

diff -r 9a6783fdb9a5 -r 222b715b5d24 src/HOL/subset.thy
--- a/src/HOL/subset.thy	Mon Oct 04 21:46:13 1999 +0200
+++ b/src/HOL/subset.thy	Mon Oct 04 21:46:49 1999 +0200
@@ -4,4 +4,7 @@
     Copyright   1994  University of Cambridge
 *)
 
-subset = Set
+theory subset = Set
+files "Tools/typedef_package.ML":
+
+end