changeset 10011 | ed5262aee27f |
parent 9970 | dfe4747c8318 |
child 10062 | 3b819da9c71a |
--- 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;