# HG changeset patch
# User wenzelm
# Date 969222292 -7200
# Node ID ed5262aee27f52087c6ef789d013a443e0f2e850
# Parent  f6ccb6df9cb964e728c8d5a5a8035bd6991db4bb
AddXIs [ext];

diff -r f6ccb6df9cb9 -r ed5262aee27f src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Sun Sep 17 22:23:48 2000 +0200
+++ b/src/HOL/HOL.ML	Sun Sep 17 22:24:52 2000 +0200
@@ -1,3 +1,7 @@
+(*  Title:      HOL/HOL.ML
+    ID:         $Id$
+*)
+
 structure HOL =
 struct
   val thy = the_context ();
@@ -27,6 +31,6 @@
   val arbitrary_def = arbitrary_def;
 end;
 
-AddXIs [disjI1, disjI2];
+AddXIs [disjI1, disjI2, ext];
 
 open HOL;