--- a/doc-src/IsarRef/IsaMakefile Tue May 31 22:18:37 2011 +0200
+++ b/doc-src/IsarRef/IsaMakefile Tue May 31 22:47:18 2011 +0200
@@ -25,8 +25,8 @@
Thy/First_Order_Logic.thy Thy/Framework.thy Thy/Inner_Syntax.thy \
Thy/Preface.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy \
Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy \
- Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Symbols.thy \
- Thy/ML_Tactic.thy
+ Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Synopsis.thy \
+ Thy/Symbols.thy Thy/ML_Tactic.thy
@$(USEDIR) -s IsarRef HOL Thy
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
Thy/document/pdfsetup.sty Thy/document/session.tex
--- a/doc-src/IsarRef/Makefile Tue May 31 22:18:37 2011 +0200
+++ b/doc-src/IsarRef/Makefile Tue May 31 22:47:18 2011 +0200
@@ -13,12 +13,13 @@
Thy/document/Generic.tex Thy/document/HOLCF_Specific.tex \
Thy/document/HOL_Specific.tex Thy/document/ML_Tactic.tex \
Thy/document/Proof.tex Thy/document/Quick_Reference.tex \
- Thy/document/Spec.tex Thy/document/ZF_Specific.tex \
- Thy/document/Inner_Syntax.tex Thy/document/Preface.tex \
- Thy/document/Document_Preparation.tex Thy/document/Misc.tex \
- Thy/document/Outer_Syntax.tex Thy/document/Symbols.tex ../isar.sty \
- ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty \
- ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty \
+ Thy/document/Spec.tex Thy/document/Synopsis.tex \
+ Thy/document/ZF_Specific.tex Thy/document/Inner_Syntax.tex \
+ Thy/document/Preface.tex Thy/document/Document_Preparation.tex \
+ Thy/document/Misc.tex Thy/document/Outer_Syntax.tex \
+ Thy/document/Symbols.tex ../isar.sty ../proof.sty ../iman.sty \
+ ../extra.sty ../ttbox.sty ../../lib/texinputs/isabelle.sty \
+ ../../lib/texinputs/isabellesym.sty \
../../lib/texinputs/railsetup.sty ../pdfsetup.sty ../manual.bib
OUTPUT = syms.tex
--- a/doc-src/IsarRef/Thy/ROOT.ML Tue May 31 22:18:37 2011 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML Tue May 31 22:47:18 2011 +0200
@@ -2,6 +2,7 @@
use_thys [
"Preface",
+ "Synopsis",
"Framework",
"First_Order_Logic",
"Outer_Syntax",
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/Synopsis.thy Tue May 31 22:47:18 2011 +0200
@@ -0,0 +1,216 @@
+theory Synopsis
+imports Base Main
+begin
+
+chapter {* Synopsis *}
+
+section {* Notepad *}
+
+text {*
+ An Isar proof body serves as mathematical notepad to compose logical
+ content, consisting of facts, terms, types.
+*}
+
+
+subsection {* Facts *}
+
+text {*
+ A fact is a simultaneous list of theorems.
+*}
+
+
+subsubsection {* Producing facts *}
+
+notepad
+begin
+
+ txt {* Via assumption (``lambda''): *}
+ assume a: A
+
+ txt {* Via proof (``let''): *}
+ have b: B sorry
+
+ txt {* Via abbreviation (``let''): *}
+ note c = a b
+
+end
+
+
+subsubsection {* Referencing facts *}
+
+notepad
+begin
+ txt {* Via explicit name: *}
+ assume a: A
+ note a
+
+ txt {* Via implicit name: *}
+ assume A
+ note this
+
+ txt {* Via literal proposition (unification with results from the proof text): *}
+ assume A
+ note `A`
+
+ assume "\<And>x. B x"
+ note `B a`
+ note `B b`
+end
+
+
+subsubsection {* Manipulating facts *}
+
+notepad
+begin
+ txt {* Instantiation: *}
+ assume a: "\<And>x. B x"
+ note a
+ note a [of b]
+ note a [where x = b]
+
+ txt {* Backchaining: *}
+ assume 1: A
+ assume 2: "A \<Longrightarrow> C"
+ note 2 [OF 1]
+ note 1 [THEN 2]
+
+ txt {* Symmetric results: *}
+ assume "x = y"
+ note this [symmetric]
+
+ assume "x \<noteq> y"
+ note this [symmetric]
+
+ txt {* Adhoc-simplication (take care!): *}
+ assume "P ([] @ xs)"
+ note this [simplified]
+end
+
+
+subsubsection {* Projections *}
+
+text {*
+ Isar facts consist of multiple theorems. There is notation to project
+ interval ranges.
+*}
+
+notepad
+begin
+ assume stuff: A B C D
+ note stuff(1)
+ note stuff(2-3)
+ note stuff(2-)
+end
+
+
+subsubsection {* Naming conventions *}
+
+text {*
+ \begin{itemize}
+
+ \item Lower-case identifiers are usually preferred.
+
+ \item Facts can be named after the main term within the proposition.
+
+ \item Facts should \emph{not} be named after the command that
+ introduced them (@{command "assume"}, @{command "have"}). This is
+ misleading and hard to maintain.
+
+ \item Natural numbers can be used as ``meaningless'' names (more
+ appropriate than @{text "a1"}, @{text "a2"} etc.)
+
+ \item Symbolic identifiers are supported (e.g. @{text "*"}, @{text
+ "**"}, @{text "***"}).
+
+ \end{itemize}
+*}
+
+
+subsection {* Block structure *}
+
+text {*
+ The formal notepad is block structured. The fact produced by the last
+ entry of a block is exported into the outer context.
+*}
+
+notepad
+begin
+ {
+ have a: A sorry
+ have b: B sorry
+ note a b
+ }
+ note this
+ note `A`
+ note `B`
+end
+
+text {* Explicit blocks as well as implicit blocks of nested goal
+ statements (e.g.\ @{command have}) automatically introduce one extra
+ pair of parentheses in reserve. The @{command next} command allows
+ to ``jump'' between these sub-blocks. *}
+
+notepad
+begin
+
+ {
+ have a: A sorry
+ next
+ have b: B
+ proof -
+ show B sorry
+ next
+ have c: C sorry
+ next
+ have d: D sorry
+ qed
+ }
+
+ txt {* Alternative version with explicit parentheses everywhere: *}
+
+ {
+ {
+ have a: A sorry
+ }
+ {
+ have b: B
+ proof -
+ {
+ show B sorry
+ }
+ {
+ have c: C sorry
+ }
+ {
+ have d: D sorry
+ }
+ qed
+ }
+ }
+
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex Tue May 31 22:47:18 2011 +0200
@@ -0,0 +1,503 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Synopsis}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Synopsis\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Synopsis%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Notepad%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+An Isar proof body serves as mathematical notepad to compose logical
+ content, consisting of facts, terms, types.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Facts%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A fact is a simultaneous list of theorems.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Producing facts%
+}
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+Via assumption (``lambda''):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{assume}\isamarkupfalse%
+\ a{\isaliteral{3A}{\isacharcolon}}\ A%
+\begin{isamarkuptxt}%
+Via proof (``let''):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{have}\isamarkupfalse%
+\ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+Via abbreviation (``let''):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{note}\isamarkupfalse%
+\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ b%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Referencing facts%
+}
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+Via explicit name:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{assume}\isamarkupfalse%
+\ a{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ a%
+\begin{isamarkuptxt}%
+Via implicit name:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{assume}\isamarkupfalse%
+\ A\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ this%
+\begin{isamarkuptxt}%
+Via literal proposition (unification with results from the proof text):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{assume}\isamarkupfalse%
+\ A\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}B\ a{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}B\ b{\isaliteral{60}{\isacharbackquoteclose}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Manipulating facts%
+}
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+Instantiation:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{assume}\isamarkupfalse%
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ a\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ a\ {\isaliteral{5B}{\isacharbrackleft}}of\ b{\isaliteral{5D}{\isacharbrackright}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ a\ {\isaliteral{5B}{\isacharbrackleft}}\isakeyword{where}\ x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5D}{\isacharbrackright}}%
+\begin{isamarkuptxt}%
+Backchaining:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ {\isadigit{2}}\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ {\isadigit{1}}\ {\isaliteral{5B}{\isacharbrackleft}}THEN\ {\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}%
+\begin{isamarkuptxt}%
+Symmetric results:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}\isanewline
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}%
+\begin{isamarkuptxt}%
+Adhoc-simplication (take care!):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ this\ {\isaliteral{5B}{\isacharbrackleft}}simplified{\isaliteral{5D}{\isacharbrackright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Projections%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isar facts consist of multiple theorems. There is notation to project
+ interval ranges.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{assume}\isamarkupfalse%
+\ stuff{\isaliteral{3A}{\isacharcolon}}\ A\ B\ C\ D\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Naming conventions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{itemize}
+
+ \item Lower-case identifiers are usually preferred.
+
+ \item Facts can be named after the main term within the proposition.
+
+ \item Facts should \emph{not} be named after the command that
+ introduced them (\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}). This is
+ misleading and hard to maintain.
+
+ \item Natural numbers can be used as ``meaningless'' names (more
+ appropriate than \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} etc.)
+
+ \item Symbolic identifiers are supported (e.g. \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}).
+
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Block structure%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The formal notepad is block structured. The fact produced by the last
+ entry of a block is exported into the outer context.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{note}\isamarkupfalse%
+\ a\ b\isanewline
+\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ this\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimproof
+\isanewline
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline
+\ \ \ \ \isacommand{proof}\isamarkupfalse%
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
+\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ B\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
+\ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
+\ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+Alternative version with explicit parentheses everywhere:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
+\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
+\ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline
+\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
+\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ B\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
+\ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
+\ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\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
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarRef/isar-ref.tex Tue May 31 22:18:37 2011 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Tue May 31 22:47:18 2011 +0200
@@ -52,6 +52,7 @@
\clearfirst
\part{Basic Concepts}
+\input{Thy/document/Synopsis.tex}
\input{Thy/document/Framework.tex}
\input{Thy/document/First_Order_Logic.tex}
\part{General Language Elements}