# HG changeset patch # User wenzelm # Date 1306874838 -7200 # Node ID ba23e83b0868f564bc51ce812bd05faf7c8b5a71 # Parent e44ec5b2cd9f812e11878c31db7b59d9fefc7b66 added Synopsis, with some "Notepad" material; diff -r e44ec5b2cd9f -r ba23e83b0868 doc-src/IsarRef/IsaMakefile --- 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 diff -r e44ec5b2cd9f -r ba23e83b0868 doc-src/IsarRef/Makefile --- 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 diff -r e44ec5b2cd9f -r ba23e83b0868 doc-src/IsarRef/Thy/ROOT.ML --- 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", diff -r e44ec5b2cd9f -r ba23e83b0868 doc-src/IsarRef/Thy/Synopsis.thy --- /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 "\x. B x" + note `B a` + note `B b` +end + + +subsubsection {* Manipulating facts *} + +notepad +begin + txt {* Instantiation: *} + assume a: "\x. B x" + note a + note a [of b] + note a [where x = b] + + txt {* Backchaining: *} + assume 1: A + assume 2: "A \ C" + note 2 [OF 1] + note 1 [THEN 2] + + txt {* Symmetric results: *} + assume "x = y" + note this [symmetric] + + assume "x \ 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 \ "t::'a" + + txt {* Abbreviations (polymorphic): *} + let ?f = "\x. x" + term "?f ?f" + + txt {* Notation: *} + write x ("***") +end + +end \ No newline at end of file diff -r e44ec5b2cd9f -r ba23e83b0868 doc-src/IsarRef/Thy/document/Synopsis.tex --- /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: diff -r e44ec5b2cd9f -r ba23e83b0868 doc-src/IsarRef/isar-ref.tex --- 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}