# HG changeset patch
# User wenzelm
# Date 1306923648 -7200
# Node ID 36daee4cc9c9af6090121bdf179e7c8d66ebd3fc
# Parent  ba23e83b0868f564bc51ce812bd05faf7c8b5a71
tuned;

diff -r ba23e83b0868 -r 36daee4cc9c9 doc-src/IsarRef/Thy/Synopsis.thy
--- a/doc-src/IsarRef/Thy/Synopsis.thy	Tue May 31 22:47:18 2011 +0200
+++ b/doc-src/IsarRef/Thy/Synopsis.thy	Wed Jun 01 12:20:48 2011 +0200
@@ -8,10 +8,33 @@
 
 text {*
   An Isar proof body serves as mathematical notepad to compose logical
-  content, consisting of facts, terms, types.
+  content, consisting of types, terms, facts.
 *}
 
 
+subsection {* Types and terms *}
+
+notepad
+begin
+  txt {* Locally fixed entities: *}
+  fix x   -- {* local constant, without any type information yet *}
+  fix x :: 'a  -- {* variant with explicit type-constraint for subsequent use*}
+
+  fix a b
+  assume "a = b"  -- {* type assignment at first occurrence in concrete term *}
+
+  txt {* Definitions (non-polymorphic): *}
+  def x \<equiv> "t::'a"
+
+  txt {* Abbreviations (polymorphic): *}
+  let ?f = "\<lambda>x. x"
+  term "?f ?f"
+
+  txt {* Notation: *}
+  write x  ("***")
+end
+
+
 subsection {* Facts *}
 
 text {*
@@ -190,27 +213,4 @@
 
 end
 
-
-subsection {* Terms and Types *}
-
-notepad
-begin
-  txt {* Locally fixed entities: *}
-  fix x   -- {* local constant, without any type information yet *}
-  fix x :: 'a  -- {* variant with explicit type-constraint for subsequent use*}
-
-  fix a b
-  assume "a = b"  -- {* type assignment at first occurrence in concrete term *}
-
-  txt {* Definitions (non-polymorphic): *}
-  def x \<equiv> "t::'a"
-
-  txt {* Abbreviations (polymorphic): *}
-  let ?f = "\<lambda>x. x"
-  term "?f ?f"
-
-  txt {* Notation: *}
-  write x  ("***")
-end
-
 end
\ No newline at end of file
diff -r ba23e83b0868 -r 36daee4cc9c9 doc-src/IsarRef/Thy/document/Synopsis.tex
--- a/doc-src/IsarRef/Thy/document/Synopsis.tex	Tue May 31 22:47:18 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex	Wed Jun 01 12:20:48 2011 +0200
@@ -28,10 +28,86 @@
 %
 \begin{isamarkuptext}%
 An Isar proof body serves as mathematical notepad to compose logical
-  content, consisting of facts, terms, types.%
+  content, consisting of types, terms, facts.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Types and terms%
+}
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+Locally fixed entities:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{fix}\isamarkupfalse%
+\ x\ \ \ %
+\isamarkupcmt{local constant, without any type information yet%
+}
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \ %
+\isamarkupcmt{variant with explicit type-constraint for subsequent use%
+}
+\isanewline
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ a\ b\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
+\isamarkupcmt{type assignment at first occurrence in concrete term%
+}
+%
+\begin{isamarkuptxt}%
+Definitions (non-polymorphic):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{def}\isamarkupfalse%
+\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{22}{\isachardoublequoteopen}}t{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptxt}%
+Abbreviations (polymorphic):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{let}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\ \ \isacommand{term}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+Notation:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{write}\isamarkupfalse%
+\ x\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
 \isamarkupsubsection{Facts%
 }
 \isamarkuptrue%
@@ -308,7 +384,7 @@
 Explicit blocks as well as implicit blocks of nested goal
   statements (e.g.\ \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}) automatically introduce one extra
   pair of parentheses in reserve.  The \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} command allows
-  to ``jump'' these sub-blocks.%
+  to ``jump'' between these sub-blocks.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{notepad}\isamarkupfalse%
@@ -404,82 +480,6 @@
 \endisadelimproof
 \isanewline
 \isacommand{end}\isamarkupfalse%
-%
-\isamarkupsubsection{Terms and Types%
-}
-\isamarkuptrue%
-\isacommand{notepad}\isamarkupfalse%
-\isanewline
-\isakeyword{begin}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-Locally fixed entities:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\ \ \ %
-\isamarkupcmt{local constant, without any type information yet%
-}
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \ %
-\isamarkupcmt{variant with explicit type-constraint for subsequent use%
-}
-\isanewline
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ a\ b\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
-\isamarkupcmt{type assignment at first occurrence in concrete term%
-}
-%
-\begin{isamarkuptxt}%
-Definitions (non-polymorphic):%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \isacommand{def}\isamarkupfalse%
-\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{22}{\isachardoublequoteopen}}t{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptxt}%
-Abbreviations (polymorphic):%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \isacommand{let}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\ \ \isacommand{term}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-Notation:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \isacommand{write}\isamarkupfalse%
-\ x\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isacommand{end}\isamarkupfalse%
 \isanewline
 %
 \isadelimtheory