# 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 \ \ A" +theorem tnd: "A \ \ A" proof - let ?P = "\X. X = False \ X = True \ A" let ?Q = "\X. X = False \ A \ 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 \ \ 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