--- a/src/HOL/Plain.thy Mon Feb 09 11:15:13 2009 +0000
+++ b/src/HOL/Plain.thy Mon Feb 09 15:38:26 2009 +0000
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record Extraction Divides
+imports Datatype FunDef Record Extraction Divides Fact
begin
text {*