src/HOL/ex/ROOT.ML
changeset 24528 e8197c9f1b5c
parent 24478 fb5e3fcfc10c
child 24530 1bac25879117
--- a/src/HOL/ex/ROOT.ML	Wed Sep 05 15:46:32 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed Sep 05 20:48:25 2007 +0200
@@ -4,7 +4,7 @@
 Miscellaneous examples for Higher-Order Logic.
 *)
 
-no_document use_thys  [
+no_document use_thys [
   "Parity",
   "GCD"
 ];