src/HOL/HOL.ML
changeset 10011 ed5262aee27f
parent 9970 dfe4747c8318
child 10062 3b819da9c71a
     1.1 --- a/src/HOL/HOL.ML	Sun Sep 17 22:23:48 2000 +0200
     1.2 +++ b/src/HOL/HOL.ML	Sun Sep 17 22:24:52 2000 +0200
     1.3 @@ -1,3 +1,7 @@
     1.4 +(*  Title:      HOL/HOL.ML
     1.5 +    ID:         $Id$
     1.6 +*)
     1.7 +
     1.8  structure HOL =
     1.9  struct
    1.10    val thy = the_context ();
    1.11 @@ -27,6 +31,6 @@
    1.12    val arbitrary_def = arbitrary_def;
    1.13  end;
    1.14  
    1.15 -AddXIs [disjI1, disjI2];
    1.16 +AddXIs [disjI1, disjI2, ext];
    1.17  
    1.18  open HOL;