# HG changeset patch # User wenzelm # Date 1284125934 -7200 # Node ID 878d86983dc1b17bc866045e56e15d8df15b30a7 # Parent cc7abfe6d5e7ea432441a29ed8bdf40a7cfcf87a updated config options; diff -r cc7abfe6d5e7 -r 878d86983dc1 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Sep 10 15:36:49 2010 +0200 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Sep 10 15:38:54 2010 +0200 @@ -106,8 +106,8 @@ @{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_hyps: "bool Config.T"} & default @{ML false} \\ + @{index_ML show_tags: "bool Config.T"} & default @{ML false} \\ @{index_ML show_question_marks: "bool Config.T"} & default @{ML true} \\ \end{mldecls} diff -r cc7abfe6d5e7 -r 878d86983dc1 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Sep 10 15:36:49 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Sep 10 15:38:54 2010 +0200 @@ -128,8 +128,8 @@ \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\_hyps}\verb|show_hyps: bool Config.T| & default \verb|false| \\ + \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Config.T| & default \verb|false| \\ \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\ \end{mldecls}