--- a/src/FOL/FOL.thy Mon Nov 03 12:26:45 1997 +0100 +++ b/src/FOL/FOL.thy Mon Nov 03 12:26:58 1997 +0100 @@ -1,4 +1,9 @@ + FOL = IFOL + + rules -classical "(~P ==> P) ==> P" + classical "(~P ==> P) ==> P" + end + +ML val thy_data = [ClasetThyData.thy_data];