src/HOL/HOL.ML

   val Let_def = Let_def;
   val if_def = if_def;
   val arbitrary_def = arbitrary_def;
 end;
 
+AddXIs [disjI1, disjI2];
+
 open HOL;