# HG changeset patch # User wenzelm # Date 1368374213 -7200 # Node ID 5b1ac9843f0276d3e0de752e8b6a810fdf3e90c7 # Parent 45b972dc78882f7470d80ff8fd7cc6ce0fe804b1 tuned comments; diff -r 45b972dc7888 -r 5b1ac9843f02 src/Pure/System/options.ML --- a/src/Pure/System/options.ML Sun May 12 17:51:34 2013 +0200 +++ b/src/Pure/System/options.ML Sun May 12 17:56:53 2013 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/System/options.ML Author: Makarius -Stand-alone options with external string representation. +System options with external string representation. *) signature OPTIONS = diff -r 45b972dc7888 -r 5b1ac9843f02 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sun May 12 17:51:34 2013 +0200 +++ b/src/Pure/System/options.scala Sun May 12 17:56:53 2013 +0200 @@ -1,7 +1,7 @@ /* Title: Pure/System/options.scala Author: Makarius -Stand-alone options with external string representation. +System options with external string representation. */ package isabelle