prefer doc-src/pdfsetup.sty;
moved IsarRef/Thy/ZF_Specific.thy to ZF/ZF_Isar.thy to avoid dependence of IsarRef on another object-logic;
--- a/doc-src/Classes/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/Classes/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -15,6 +15,8 @@
cp "$ISABELLE_HOME/doc-src/manual.bib" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/Codegen/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/Codegen/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -22,6 +22,8 @@
done
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/Functions/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/Functions/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -11,6 +11,8 @@
cp "$ISABELLE_HOME/doc-src/manual.bib" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/HOL/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/HOL/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -16,6 +16,8 @@
cp "$ISABELLE_HOME/doc-src/Logics/document/syntax.tex" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/Intro/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/Intro/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -15,6 +15,8 @@
cp "$ISABELLE_HOME/doc-src/manual.bib" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/IsarImplementation/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/IsarImplementation/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -17,6 +17,8 @@
cp "$ISABELLE_HOME/doc-src/manual.bib" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/IsarRef/Makefile Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/IsarRef/Makefile Tue Aug 28 12:22:10 2012 +0200
@@ -14,7 +14,7 @@
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/Synopsis.tex \
- Thy/document/ZF_Specific.tex Thy/document/Inner_Syntax.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 \
--- a/doc-src/IsarRef/Thy/Base.thy Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/IsarRef/Thy/Base.thy Tue Aug 28 12:22:10 2012 +0200
@@ -3,12 +3,6 @@
begin
ML_file "../../antiquote_setup.ML"
-
-setup {*
- Antiquote_Setup.setup #>
- member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
-*}
-
-declare [[thy_output_source]]
+setup Antiquote_Setup.setup
end
--- a/doc-src/IsarRef/Thy/ZF_Specific.thy Mon Aug 27 23:37:16 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-theory ZF_Specific
-imports Base Main
-begin
-
-chapter {* Isabelle/ZF \label{ch:zf} *}
-
-section {* Type checking *}
-
-text {*
- The ZF logic is essentially untyped, so the concept of ``type
- checking'' is performed as logical reasoning about set-membership
- statements. A special method assists users in this task; a version
- of this is already declared as a ``solver'' in the standard
- Simplifier setup.
-
- \begin{matharray}{rcl}
- @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{method_def (ZF) typecheck} & : & @{text method} \\
- @{attribute_def (ZF) TC} & : & @{text attribute} \\
- \end{matharray}
-
- @{rail "
- @@{attribute (ZF) TC} (() | 'add' | 'del')
- "}
-
- \begin{description}
-
- \item @{command (ZF) "print_tcset"} prints the collection of
- typechecking rules of the current context.
-
- \item @{method (ZF) typecheck} attempts to solve any pending
- type-checking problems in subgoals.
-
- \item @{attribute (ZF) TC} adds or deletes type-checking rules from
- the context.
-
- \end{description}
-*}
-
-
-section {* (Co)Inductive sets and datatypes *}
-
-subsection {* Set definitions *}
-
-text {*
- In ZF everything is a set. The generic inductive package also
- provides a specific view for ``datatype'' specifications.
- Coinductive definitions are available in both cases, too.
-
- \begin{matharray}{rcl}
- @{command_def (ZF) "inductive"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (ZF) "coinductive"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (ZF) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (ZF) "codatatype"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
- @{rail "
- (@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints
- ;
-
- domains: @'domains' (@{syntax term} + '+') ('<=' | '\<subseteq>') @{syntax term}
- ;
- intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
- ;
- hints: @{syntax (ZF) \"monos\"}? condefs? \\
- @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
- ;
- @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs}
- ;
- condefs: @'con_defs' @{syntax thmrefs}
- ;
- @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs}
- ;
- @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs}
- "}
-
- In the following syntax specification @{text "monos"}, @{text
- typeintros}, and @{text typeelims} are the same as above.
-
- @{rail "
- (@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints
- ;
-
- domain: ('<=' | '\<subseteq>') @{syntax term}
- ;
- dtspec: @{syntax term} '=' (con + '|')
- ;
- con: @{syntax name} ('(' (@{syntax term} ',' +) ')')?
- ;
- hints: @{syntax (ZF) \"monos\"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
- "}
-
- See \cite{isabelle-ZF} for further information on inductive
- definitions in ZF, but note that this covers the old-style theory
- format.
-*}
-
-
-subsection {* Primitive recursive functions *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
- @{rail "
- @@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +)
- "}
-*}
-
-
-subsection {* Cases and induction: emulating tactic scripts *}
-
-text {*
- The following important tactical tools of Isabelle/ZF have been
- ported to Isar. These should not be used in proper proof texts.
-
- \begin{matharray}{rcl}
- @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
- @{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
- @{rail "
- (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name}
- ;
- @@{method (ZF) ind_cases} (@{syntax prop} +)
- ;
- @@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and')
- ;
- "}
-*}
-
-end
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Mon Aug 27 23:37:16 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,334 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{ZF{\isaliteral{5F}{\isacharunderscore}}Specific}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ ZF{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
-\isakeyword{imports}\ Base\ Main\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupchapter{Isabelle/ZF \label{ch:zf}%
-}
-\isamarkuptrue%
-%
-\isamarkupsection{Type checking%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The ZF logic is essentially untyped, so the concept of ``type
- checking'' is performed as logical reasoning about set-membership
- statements. A special method assists users in this task; a version
- of this is already declared as a ``solver'' in the standard
- Simplifier setup.
-
- \begin{matharray}{rcl}
- \indexdef{ZF}{command}{print\_tcset}\hypertarget{command.ZF.print-tcset}{\hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}tcset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{ZF}{method}{typecheck}\hypertarget{method.ZF.typecheck}{\hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}}} & : & \isa{method} \\
- \indexdef{ZF}{attribute}{TC}\hypertarget{attribute.ZF.TC}{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}} & : & \isa{attribute} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{3}{}
-\rail@term{\hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{add}}[]
-\rail@nextbar{2}
-\rail@term{\isa{del}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}
-
-
- \begin{description}
-
- \item \hyperlink{command.ZF.print-tcset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}tcset}}}} prints the collection of
- typechecking rules of the current context.
-
- \item \hyperlink{method.ZF.typecheck}{\mbox{\isa{typecheck}}} attempts to solve any pending
- type-checking problems in subgoals.
-
- \item \hyperlink{attribute.ZF.TC}{\mbox{\isa{TC}}} adds or deletes type-checking rules from
- the context.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{(Co)Inductive sets and datatypes%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Set definitions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In ZF everything is a set. The generic inductive package also
- provides a specific view for ``datatype'' specifications.
- Coinductive definitions are available in both cases, too.
-
- \begin{matharray}{rcl}
- \indexdef{ZF}{command}{inductive}\hypertarget{command.ZF.inductive}{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{ZF}{command}{coinductive}\hypertarget{command.ZF.coinductive}{\hyperlink{command.ZF.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{ZF}{command}{datatype}\hypertarget{command.ZF.datatype}{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{ZF}{command}{codatatype}\hypertarget{command.ZF.codatatype}{\hyperlink{command.ZF.codatatype}{\mbox{\isa{\isacommand{codatatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{2}{}
-\rail@bar
-\rail@term{\hyperlink{command.ZF.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{command.ZF.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
-\rail@endbar
-\rail@nont{\isa{domains}}[]
-\rail@nont{\isa{intros}}[]
-\rail@nont{\isa{hints}}[]
-\rail@end
-\rail@begin{2}{\isa{domains}}
-\rail@term{\isa{\isakeyword{domains}}}[]
-\rail@plus
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextplus{1}
-\rail@cterm{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
-\rail@endplus
-\rail@bar
-\rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@end
-\rail@begin{3}{\isa{intros}}
-\rail@term{\isa{\isakeyword{intros}}}[]
-\rail@plus
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextplus{2}
-\rail@endplus
-\rail@end
-\rail@begin{5}{\isa{hints}}
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{condefs}}[]
-\rail@endbar
-\rail@cr{3}
-\rail@bar
-\rail@nextbar{4}
-\rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{4}
-\rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[]
-\rail@endbar
-\rail@end
-\rail@begin{1}{\indexdef{ZF}{syntax}{monos}\hypertarget{syntax.ZF.monos}{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}}
-\rail@term{\isa{\isakeyword{monos}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@end
-\rail@begin{1}{\isa{condefs}}
-\rail@term{\isa{\isakeyword{con{\isaliteral{5F}{\isacharunderscore}}defs}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@end
-\rail@begin{1}{\indexdef{ZF}{syntax}{typeintros}\hypertarget{syntax.ZF.typeintros}{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}}
-\rail@term{\isa{\isakeyword{type{\isaliteral{5F}{\isacharunderscore}}intros}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@end
-\rail@begin{1}{\indexdef{ZF}{syntax}{typeelims}\hypertarget{syntax.ZF.typeelims}{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}}
-\rail@term{\isa{\isakeyword{type{\isaliteral{5F}{\isacharunderscore}}elims}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@end
-\end{railoutput}
-
-
- In the following syntax specification \isa{{\isaliteral{22}{\isachardoublequote}}monos{\isaliteral{22}{\isachardoublequote}}}, \isa{typeintros}, and \isa{typeelims} are the same as above.
-
- \begin{railoutput}
-\rail@begin{2}{}
-\rail@bar
-\rail@term{\hyperlink{command.ZF.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{command.ZF.codatatype}{\mbox{\isa{\isacommand{codatatype}}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{domain}}[]
-\rail@endbar
-\rail@plus
-\rail@nont{\isa{dtspec}}[]
-\rail@nextplus{1}
-\rail@cterm{\isa{\isakeyword{and}}}[]
-\rail@endplus
-\rail@nont{\isa{hints}}[]
-\rail@end
-\rail@begin{2}{\isa{domain}}
-\rail@bar
-\rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@end
-\rail@begin{2}{\isa{dtspec}}
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@plus
-\rail@nont{\isa{con}}[]
-\rail@nextplus{1}
-\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
-\rail@endplus
-\rail@end
-\rail@begin{3}{\isa{con}}
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@plus
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@term{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
-\rail@nextplus{2}
-\rail@endplus
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
-\rail@end
-\rail@begin{2}{\isa{hints}}
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.ZF.monos}{\mbox{\isa{monos}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.ZF.typeintros}{\mbox{\isa{typeintros}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.ZF.typeelims}{\mbox{\isa{typeelims}}}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}
-
-
- See \cite{isabelle-ZF} for further information on inductive
- definitions in ZF, but note that this covers the old-style theory
- format.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Primitive recursive functions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{ZF}{command}{primrec}\hypertarget{command.ZF.primrec}{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{3}{}
-\rail@term{\hyperlink{command.ZF.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
-\rail@plus
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextplus{2}
-\rail@endplus
-\rail@end
-\end{railoutput}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Cases and induction: emulating tactic scripts%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The following important tactical tools of Isabelle/ZF have been
- ported to Isar. These should not be used in proper proof texts.
-
- \begin{matharray}{rcl}
- \indexdef{ZF}{method}{case\_tac}\hypertarget{method.ZF.case-tac}{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
- \indexdef{ZF}{method}{induct\_tac}\hypertarget{method.ZF.induct-tac}{\hyperlink{method.ZF.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
- \indexdef{ZF}{method}{ind\_cases}\hypertarget{method.ZF.ind-cases}{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
- \indexdef{ZF}{command}{inductive\_cases}\hypertarget{command.ZF.inductive-cases}{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{2}{}
-\rail@bar
-\rail@term{\hyperlink{method.ZF.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{method.ZF.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{method.ZF.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
-\rail@plus
-\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@end
-\rail@begin{3}{}
-\rail@term{\hyperlink{command.ZF.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
-\rail@plus
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
-\rail@endbar
-\rail@plus
-\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@nextplus{2}
-\rail@cterm{\isa{\isakeyword{and}}}[]
-\rail@endplus
-\rail@end
-\end{railoutput}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/IsarRef/isar-ref.tex Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Tue Aug 28 12:22:10 2012 +0200
@@ -72,7 +72,6 @@
\part{Object-Logics}
\input{Thy/document/HOL_Specific.tex}
\input{Thy/document/HOLCF_Specific.tex}
-\input{Thy/document/ZF_Specific.tex}
\part{Appendix}
\appendix
--- a/doc-src/LaTeXsugar/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/LaTeXsugar/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -6,6 +6,8 @@
VARIANT="$2"
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/Locales/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/Locales/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -6,6 +6,8 @@
VARIANT="$2"
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/Logics/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/Logics/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -15,6 +15,8 @@
cp "$ISABELLE_HOME/doc-src/manual.bib" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/Main/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/Main/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -6,6 +6,8 @@
VARIANT="$2"
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/ProgProve/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/ProgProve/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -11,6 +11,8 @@
cp "$ISABELLE_HOME/doc-src/ProgProve/MyList.thy" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/ROOT Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/ROOT Tue Aug 28 12:22:10 2012 +0200
@@ -3,6 +3,7 @@
theories [document = false] Setup
theories Classes
files
+ "../pdfsetup.sty"
"document/build"
"document/root.tex"
"document/style.sty"
@@ -19,6 +20,7 @@
Adaptation
Further
files
+ "../pdfsetup.sty"
"document/adapt.tex"
"document/architecture.tex"
"document/build"
@@ -29,6 +31,7 @@
options [document_variants = "functions"]
theories Functions
files
+ "../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../isar.sty"
@@ -54,6 +57,7 @@
Syntax
Tactic
files
+ "../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../isar.sty"
@@ -69,6 +73,7 @@
options [document_variants = "intro"]
theories
files
+ "../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
@@ -80,7 +85,7 @@
session "HOL-IsarRef" (doc) in "IsarRef/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
- quick_and_dirty]
+ quick_and_dirty, thy_output_source]
theories
Preface
Synopsis
@@ -101,15 +106,9 @@
session "HOLCF-IsarRef" (doc) in "IsarRef/Thy" = HOLCF +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
- quick_and_dirty]
+ quick_and_dirty, thy_output_source]
theories HOLCF_Specific
-session "ZF-IsarRef" (doc) in "IsarRef/Thy" = ZF +
- options [browser_info = false, document = false,
- document_dump = document, document_dump_mode = "tex",
- quick_and_dirty]
- theories ZF_Specific
-
session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
options [document_variants = "sugar"]
theories [document = ""]
@@ -117,6 +116,7 @@
"~~/src/HOL/Library/OptionalSugar"
theories Sugar
files
+ "../pdfsetup.sty"
"document/build"
"document/mathpartir.sty"
"document/root.bib"
@@ -129,6 +129,7 @@
Examples2
Examples3
files
+ "../pdfsetup.sty"
"document/build"
"document/root.tex"
@@ -136,6 +137,7 @@
options [document_variants = "logics"]
theories
files
+ "../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
@@ -148,6 +150,7 @@
options [document_variants = "logics-HOL"]
theories
files
+ "../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
@@ -158,13 +161,17 @@
"document/root.tex"
session "Logics-ZF" (doc) in "ZF" = ZF +
- options [document_variants = "logics-ZF", print_mode = "brackets"]
+ options [document_variants = "logics-ZF", print_mode = "brackets",
+ thy_output_source]
theories
IFOL_examples
FOL_examples
ZF_examples
If
+ ZF_Isar
files
+ "../pdfsetup.sty"
+ "../isar.sty"
"../ttbox.sty"
"../proof.sty"
"../manual.bib"
@@ -176,6 +183,7 @@
options [document_variants = "main"]
theories Main_Doc
files
+ "../pdfsetup.sty"
"document/build"
"document/root.tex"
@@ -189,6 +197,7 @@
Logic
Isar
files
+ "../pdfsetup.sty"
"document/bang.eps"
"document/bang.pdf"
"document/build"
@@ -203,6 +212,7 @@
options [document_variants = "ref"]
theories
files
+ "../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
@@ -228,6 +238,7 @@
Misc
files
"../IsarRef/style.sty"
+ "../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
--- a/doc-src/Ref/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/Ref/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -15,6 +15,8 @@
cp "$ISABELLE_HOME/doc-src/manual.bib" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/System/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/System/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -17,6 +17,8 @@
cp "$ISABELLE_HOME/doc-src/manual.bib" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/ZF_Isar.thy Tue Aug 28 12:22:10 2012 +0200
@@ -0,0 +1,140 @@
+theory ZF_Isar
+imports Main
+begin
+
+(*<*)
+ML_file "../antiquote_setup.ML"
+setup Antiquote_Setup.setup
+(*>*)
+
+chapter {* Some Isar language elements *}
+
+section {* Type checking *}
+
+text {*
+ The ZF logic is essentially untyped, so the concept of ``type
+ checking'' is performed as logical reasoning about set-membership
+ statements. A special method assists users in this task; a version
+ of this is already declared as a ``solver'' in the standard
+ Simplifier setup.
+
+ \begin{matharray}{rcl}
+ @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{method_def (ZF) typecheck} & : & @{text method} \\
+ @{attribute_def (ZF) TC} & : & @{text attribute} \\
+ \end{matharray}
+
+ @{rail "
+ @@{attribute (ZF) TC} (() | 'add' | 'del')
+ "}
+
+ \begin{description}
+
+ \item @{command (ZF) "print_tcset"} prints the collection of
+ typechecking rules of the current context.
+
+ \item @{method (ZF) typecheck} attempts to solve any pending
+ type-checking problems in subgoals.
+
+ \item @{attribute (ZF) TC} adds or deletes type-checking rules from
+ the context.
+
+ \end{description}
+*}
+
+
+section {* (Co)Inductive sets and datatypes *}
+
+subsection {* Set definitions *}
+
+text {*
+ In ZF everything is a set. The generic inductive package also
+ provides a specific view for ``datatype'' specifications.
+ Coinductive definitions are available in both cases, too.
+
+ \begin{matharray}{rcl}
+ @{command_def (ZF) "inductive"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (ZF) "coinductive"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (ZF) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (ZF) "codatatype"} & : & @{text "theory \<rightarrow> theory"} \\
+ \end{matharray}
+
+ @{rail "
+ (@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints
+ ;
+
+ domains: @'domains' (@{syntax term} + '+') ('<=' | '\<subseteq>') @{syntax term}
+ ;
+ intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
+ ;
+ hints: @{syntax (ZF) \"monos\"}? condefs? \\
+ @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
+ ;
+ @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs}
+ ;
+ condefs: @'con_defs' @{syntax thmrefs}
+ ;
+ @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs}
+ ;
+ @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs}
+ "}
+
+ In the following syntax specification @{text "monos"}, @{text
+ typeintros}, and @{text typeelims} are the same as above.
+
+ @{rail "
+ (@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints
+ ;
+
+ domain: ('<=' | '\<subseteq>') @{syntax term}
+ ;
+ dtspec: @{syntax term} '=' (con + '|')
+ ;
+ con: @{syntax name} ('(' (@{syntax term} ',' +) ')')?
+ ;
+ hints: @{syntax (ZF) \"monos\"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
+ "}
+
+ See \cite{isabelle-ZF} for further information on inductive
+ definitions in ZF, but note that this covers the old-style theory
+ format.
+*}
+
+
+subsection {* Primitive recursive functions *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\
+ \end{matharray}
+
+ @{rail "
+ @@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +)
+ "}
+*}
+
+
+subsection {* Cases and induction: emulating tactic scripts *}
+
+text {*
+ The following important tactical tools of Isabelle/ZF have been
+ ported to Isar. These should not be used in proper proof texts.
+
+ \begin{matharray}{rcl}
+ @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
+ @{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\
+ \end{matharray}
+
+ @{rail "
+ (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name}
+ ;
+ @@{method (ZF) ind_cases} (@{syntax prop} +)
+ ;
+ @@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and')
+ ;
+ "}
+*}
+
+end
--- a/doc-src/ZF/document/build Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/ZF/document/build Tue Aug 28 12:22:10 2012 +0200
@@ -8,12 +8,15 @@
"$ISABELLE_TOOL" logo -o isabelle_zf.pdf "ZF"
"$ISABELLE_TOOL" logo -o isabelle_zf.eps "ZF"
+cp "$ISABELLE_HOME/doc-src/isar.sty" .
cp "$ISABELLE_HOME/doc-src/ttbox.sty" .
cp "$ISABELLE_HOME/doc-src/proof.sty" .
cp "$ISABELLE_HOME/doc-src/manual.bib" .
cp "$ISABELLE_HOME/doc-src/Logics/document/syntax.tex" .
"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
"$ISABELLE_TOOL" latex -o "$FORMAT"
--- a/doc-src/ZF/document/root.tex Mon Aug 27 23:37:16 2012 +0200
+++ b/doc-src/ZF/document/root.tex Tue Aug 28 12:22:10 2012 +0200
@@ -1,6 +1,7 @@
\documentclass[11pt,a4paper]{report}
-\usepackage{isabelle,isabellesym}
+\usepackage{isabelle,isabellesym,railsetup}
\usepackage{graphicx,logics,ttbox,proof,latexsym}
+\usepackage{isar}
\usepackage{pdfsetup}
%last package!
@@ -36,6 +37,14 @@
\sloppy
\binperiod %%%treat . like a binary operator
+
+\isadroptag{theory}
+
+\railtermfont{\isabellestyle{tt}}
+\railnontermfont{\isabellestyle{literal}}
+\railnamefont{\isabellestyle{literal}}
+
+
\begin{document}
\maketitle
@@ -71,6 +80,11 @@
\input{syntax}
\include{FOL}
\include{ZF}
+
+\isabellestyle{literal}
+\include{ZF_Isar}
+\isabellestyle{tt}
+
\bibliographystyle{plain}
\bibliography{manual}
\printindex