# HG changeset patch
# User wenzelm
# Date 1001601826 -7200
# Node ID 4b171ad4ff6505b8e92eb62abadd92e800f0dd87
# Parent  14ae6a86813d9ab63bb28422925bbffe3919460e
tuned;

diff -r 14ae6a86813d -r 4b171ad4ff65 src/HOL/ex/Hilbert_Classical.thy
--- a/src/HOL/ex/Hilbert_Classical.thy	Thu Sep 27 16:04:44 2001 +0200
+++ b/src/HOL/ex/Hilbert_Classical.thy	Thu Sep 27 16:43:46 2001 +0200
@@ -16,7 +16,7 @@
 
 subsection {* Proof text *}
 
-theorem "A \<or> \<not> A"
+theorem tnd: "A \<or> \<not> A"
 proof -
   let ?P = "\<lambda>X. X = False \<or> X = True \<and> A"
   let ?Q = "\<lambda>X. X = False \<and> A \<or> X = True"
@@ -95,6 +95,13 @@
 qed
 
 
+subsection {* Proof term of text *}
+
+text {*
+  {\small @{prf [display, margin = 80] tnd}}
+*}
+
+
 subsection {* Proof script *}
 
 theorem tnd': "A \<or> \<not> A"
@@ -149,17 +156,10 @@
   done
 
 
-subsection {* Proof term of text *}
-
-text {*
-  @{prf [display] tnd}
-*}
-
-
 subsection {* Proof term of script *}
 
 text {*
-  @{prf [display] tnd'}
+  {\small @{prf [display, margin = 80] tnd'}}
 *}
 
 end