author | wenzelm |
Sun, 17 Sep 2000 22:24:52 +0200 | |
changeset 10011 | ed5262aee27f |
parent 10010 | f6ccb6df9cb9 |
child 10012 | 4961c73b5f60 |
src/HOL/HOL.ML | file | annotate | diff | comparison | revisions |
--- 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;