src/FOL/FOL.ML
changeset 11976 075df6e46cef
parent 11588 d792570a04b1
child 12303 67ca723a02dd
equal deleted inserted replaced
11975:129c6679e8c4 11976:075df6e46cef
     3 struct
     3 struct
     4   val thy = the_context ();
     4   val thy = the_context ();
     5   val classical = classical;
     5   val classical = classical;
     6 end;
     6 end;
     7 
     7 
     8 AddXIs [equal_intr_rule];
       
     9 AddXEs [disjI1, disjI2];
     8 AddXEs [disjI1, disjI2];
    10 
     9 
    11 open FOL;
    10 open FOL;