# HG changeset patch # User wenzelm # Date 878556418 -3600 # Node ID 5e8f3d57dee7d534ed4c6dabe4de6be2a6777fa0 # Parent 9faf228771dc4a4fbcd4043c4f2968eb3c9458d3 added claset thy_data; diff -r 9faf228771dc -r 5e8f3d57dee7 src/FOL/FOL.thy --- 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];