# HG changeset patch
# User wenzelm
# Date 1011628972 -3600
# Node ID a2a3896f9c48bdacdc037607a0a2380a457b619e
# Parent  c037ff3e5ddf629516e0780ff9086df1faaeb0e6
reset show_hyps by default (in accordance to existing Isar practice);

diff -r c037ff3e5ddf -r a2a3896f9c48 doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Mon Jan 21 16:28:22 2002 +0100
+++ b/doc-src/Ref/introduction.tex	Mon Jan 21 17:02:52 2002 +0100
@@ -252,7 +252,7 @@
 \index{meta-assumptions!printing of}
 \index{types!printing of}\index{sorts!printing of}
 \begin{ttbox} 
-show_hyps     : bool ref \hfill{\bf initially true}
+show_hyps     : bool ref \hfill{\bf initially false}
 show_tags     : bool ref \hfill{\bf initially false}
 show_brackets : bool ref \hfill{\bf initially false}
 show_types    : bool ref \hfill{\bf initially false}
diff -r c037ff3e5ddf -r a2a3896f9c48 src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Jan 21 16:28:22 2002 +0100
+++ b/src/Pure/display.ML	Mon Jan 21 17:02:52 2002 +0100
@@ -60,7 +60,7 @@
 (** print thm **)
 
 val goals_limit = ref 10;       (*max number of goals to print -- set by user*)
-val show_hyps = ref true;       (*false: print meta-hypotheses as dots*)
+val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
 val show_tags = ref false;      (*false: suppress tags*)
 
 fun pretty_tag (name, args) = Pretty.strs (name :: map quote args);