--- a/Prove.thy Fri Dec 04 18:32:19 2009 +0100 +++ b/Prove.thy Fri Dec 04 21:42:55 2009 +0100 @@ -1,5 +1,5 @@ theory Prove -imports Main +imports Plain begin ML {*