# HG changeset patch
# User wenzelm
# Date 1283554743 -7200
# Node ID 12dac4b58df8f1b979c6c155c1514211282c711a
# Parent  976af4e27cde26a750606f0ed55adfdf27cddba6
updated configuration options;

diff -r 976af4e27cde -r 12dac4b58df8 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Sep 04 00:31:21 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Sep 04 00:59:03 2010 +0200
@@ -103,9 +103,9 @@
     @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
     @{index_ML show_brackets: "bool Unsynchronized.ref"} & default @{ML false} \\
-    @{index_ML eta_contract: "bool Unsynchronized.ref"} & default @{ML true} \\
-    @{index_ML goals_limit: "int Unsynchronized.ref"} & default @{ML 10} \\
-    @{index_ML Proof.show_main_goal: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\
+    @{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\
+    @{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\
     @{index_ML show_hyps: "bool Unsynchronized.ref"} & default @{ML false} \\
     @{index_ML show_tags: "bool Unsynchronized.ref"} & default @{ML false} \\
     @{index_ML show_question_marks: "bool Config.T"} & default @{ML true} \\
@@ -173,13 +173,13 @@
   rewriting operate modulo @{text "\<alpha>\<beta>\<eta>"}-conversion, some other tools
   might look at terms more discretely.
 
-  \item @{ML goals_limit} controls the maximum number of subgoals to
-  be shown in goal output.
+  \item @{ML Goal_Display.goals_limit} controls the maximum number of
+  subgoals to be shown in goal output.
 
-  \item @{ML Proof.show_main_goal} controls whether the main result to
-  be proven should be displayed.  This information might be relevant
-  for schematic goals, to inspect the current claim that has been
-  synthesized so far.
+  \item @{ML Goal_Display.show_main_goal} controls whether the main
+  result to be proven should be displayed.  This information might be
+  relevant for schematic goals, to inspect the current claim that has
+  been synthesized so far.
 
   \item @{ML show_hyps} controls printing of implicit hypotheses of
   local facts.  Normally, only those hypotheses are displayed that are
diff -r 976af4e27cde -r 12dac4b58df8 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Sep 04 00:31:21 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Sep 04 00:59:03 2010 +0200
@@ -125,9 +125,9 @@
     \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
     \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
     \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Unsynchronized.ref| & default \verb|false| \\
-    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Unsynchronized.ref| & default \verb|true| \\
-    \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int Unsynchronized.ref| & default \verb|10| \\
-    \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
+    \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
+    \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
     \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Unsynchronized.ref| & default \verb|false| \\
     \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Unsynchronized.ref| & default \verb|false| \\
     \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
@@ -190,13 +190,13 @@
   rewriting operate modulo \isa{{\isachardoublequote}{\isasymalpha}{\isasymbeta}{\isasymeta}{\isachardoublequote}}-conversion, some other tools
   might look at terms more discretely.
 
-  \item \verb|goals_limit| controls the maximum number of subgoals to
-  be shown in goal output.
+  \item \verb|Goal_Display.goals_limit| controls the maximum number of
+  subgoals to be shown in goal output.
 
-  \item \verb|Proof.show_main_goal| controls whether the main result to
-  be proven should be displayed.  This information might be relevant
-  for schematic goals, to inspect the current claim that has been
-  synthesized so far.
+  \item \verb|Goal_Display.show_main_goal| controls whether the main
+  result to be proven should be displayed.  This information might be
+  relevant for schematic goals, to inspect the current claim that has
+  been synthesized so far.
 
   \item \verb|show_hyps| controls printing of implicit hypotheses of
   local facts.  Normally, only those hypotheses are displayed that are