--- a/doc-src/IsarImplementation/Thy/Logic.thy Tue May 03 21:40:14 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Tue May 03 21:44:05 2011 +0200
@@ -517,14 +517,14 @@
\infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
\]
\[
- \infer[@{text "(\<And>\<dash>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
+ \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
\qquad
- \infer[@{text "(\<And>\<dash>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
+ \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
\]
\[
- \infer[@{text "(\<Longrightarrow>\<dash>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
+ \infer[@{text "(\<Longrightarrow>\<hyphen>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
\qquad
- \infer[@{text "(\<Longrightarrow>\<dash>elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
+ \infer[@{text "(\<Longrightarrow>\<hyphen>elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
\]
\caption{Primitive inferences of Pure}\label{fig:prim-rules}
\end{center}
@@ -554,7 +554,7 @@
\cite{Berghofer-Nipkow:2000:TPHOL}).
Observe that locally fixed parameters (as in @{text
- "\<And>\<dash>intro"}) need not be recorded in the hypotheses, because
+ "\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because
the simple syntactic types of Pure are always inhabitable.
``Assumptions'' @{text "x :: \<tau>"} for type-membership are only
present as long as some @{text "x\<^isub>\<tau>"} occurs in the statement
--- a/doc-src/IsarImplementation/Thy/Proof.thy Tue May 03 21:40:14 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Tue May 03 21:44:05 2011 +0200
@@ -253,14 +253,14 @@
\medskip The most basic export rule discharges assumptions directly
by means of the @{text "\<Longrightarrow>"} introduction rule:
\[
- \infer[(@{text "\<Longrightarrow>\<dash>intro"})]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
+ \infer[(@{text "\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
\]
The variant for goal refinements marks the newly introduced
premises, which causes the canonical Isar goal refinement scheme to
enforce unification with local premises within the goal:
\[
- \infer[(@{text "#\<Longrightarrow>\<dash>intro"})]{@{text "\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
+ \infer[(@{text "#\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
\]
\medskip Alternative versions of assumptions may perform arbitrary
@@ -269,7 +269,7 @@
definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
with the following export rule to reverse the effect:
\[
- \infer[(@{text "\<equiv>\<dash>expand"})]{@{text "\<Gamma> - (x \<equiv> t) \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
+ \infer[(@{text "\<equiv>\<hyphen>expand"})]{@{text "\<Gamma> - (x \<equiv> t) \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
\]
This works, because the assumption @{text "x \<equiv> t"} was introduced in
a context with @{text "x"} being fresh, so @{text "x"} does not
@@ -307,7 +307,7 @@
\item @{ML Assumption.add_assumes}~@{text "As"} is a special case of
@{ML Assumption.add_assms} where the export rule performs @{text
- "\<Longrightarrow>\<dash>intro"} or @{text "#\<Longrightarrow>\<dash>intro"}, depending on goal
+ "\<Longrightarrow>\<hyphen>intro"} or @{text "#\<Longrightarrow>\<hyphen>intro"}, depending on goal
mode.
\item @{ML Assumption.export}~@{text "is_goal inner outer thm"}
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Tue May 03 21:40:14 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Tue May 03 21:44:05 2011 +0200
@@ -592,14 +592,14 @@
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}assume{\isaliteral{29}{\isacharparenright}}}]{\isa{A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}{}
\]
\[
- \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}
+ \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}
\qquad
- \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}
+ \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}
\]
\[
- \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
+ \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
\qquad
- \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}
+ \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}
\]
\caption{Primitive inferences of Pure}\label{fig:prim-rules}
\end{center}
@@ -626,7 +626,7 @@
terms, and \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} for proofs (cf.\
\cite{Berghofer-Nipkow:2000:TPHOL}).
- Observe that locally fixed parameters (as in \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro}) need not be recorded in the hypotheses, because
+ Observe that locally fixed parameters (as in \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro}) need not be recorded in the hypotheses, because
the simple syntactic types of Pure are always inhabitable.
``Assumptions'' \isa{x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} for type-membership are only
present as long as some \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} occurs in the statement
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Tue May 03 21:40:14 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Tue May 03 21:44:05 2011 +0200
@@ -397,14 +397,14 @@
\medskip The most basic export rule discharges assumptions directly
by means of the \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} introduction rule:
\[
- \infer[(\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
+ \infer[(\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
\]
The variant for goal refinements marks the newly introduced
premises, which causes the canonical Isar goal refinement scheme to
enforce unification with local premises within the goal:
\[
- \infer[(\isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
+ \infer[(\isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}
\]
\medskip Alternative versions of assumptions may perform arbitrary
@@ -413,7 +413,7 @@
definition works by fixing \isa{x} and assuming \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t},
with the following export rule to reverse the effect:
\[
- \infer[(\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{5C3C646173683E}{\isasymdash}}expand})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ t}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x}}
+ \infer[(\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}expand})]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ t}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x}}
\]
This works, because the assumption \isa{x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} was introduced in
a context with \isa{x} being fresh, so \isa{x} does not
@@ -455,7 +455,7 @@
\verb|Assumption.assume|.
\item \verb|Assumption.add_assumes|~\isa{As} is a special case of
- \verb|Assumption.add_assms| where the export rule performs \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro} or \isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C646173683E}{\isasymdash}}intro}, depending on goal
+ \verb|Assumption.add_assms| where the export rule performs \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro} or \isa{{\isaliteral{23}{\isacharhash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro}, depending on goal
mode.
\item \verb|Assumption.export|~\isa{is{\isaliteral{5F}{\isacharunderscore}}goal\ inner\ outer\ thm}
--- a/doc-src/IsarImplementation/style.sty Tue May 03 21:40:14 2011 +0200
+++ b/doc-src/IsarImplementation/style.sty Tue May 03 21:44:05 2011 +0200
@@ -65,7 +65,6 @@
\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
\isabellestyle{itunderscore}
-\newcommand{\isasymdash}{\mbox{-}}
\railtermfont{\isabellestyle{tt}}
\railnontermfont{\isabellestyle{itunderscore}}
--- a/doc-src/IsarRef/Thy/Framework.thy Tue May 03 21:40:14 2011 +0200
+++ b/doc-src/IsarRef/Thy/Framework.thy Tue May 03 21:44:05 2011 +0200
@@ -424,7 +424,7 @@
\infer[(@{inference refinement})]
{@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
{\begin{tabular}{rl}
- @{text "sub\<dash>proof:"} &
+ @{text "sub\<hyphen>proof:"} &
@{text "\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a"} \\
@{text "goal:"} &
@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
@@ -436,7 +436,7 @@
\end{tabular}}
\]
- \noindent Here the @{text "sub\<dash>proof"} rule stems from the
+ \noindent Here the @{text "sub\<hyphen>proof"} rule stems from the
main @{command fix}-@{command assume}-@{command show} outline of
Isar (cf.\ \secref{sec:framework-subproof}): each assumption
indicated in the text results in a marked premise @{text "G"} above.
@@ -466,7 +466,7 @@
\medskip
\begin{tabular}{rcl}
- @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "statement proof |"}~~@{command "definition"}~@{text "\<dots> | \<dots>"} \\[1ex]
+ @{text "theory\<hyphen>stmt"} & = & @{command "theorem"}~@{text "statement proof |"}~~@{command "definition"}~@{text "\<dots> | \<dots>"} \\[1ex]
@{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\[1ex]
@@ -582,7 +582,7 @@
\medskip
\begin{tabular}{rcl}
- @{command presume}~@{text A} & @{text "\<equiv>"} & @{command assume}~@{text "\<guillemotleft>weak\<dash>discharge\<guillemotright> A"} \\
+ @{command presume}~@{text A} & @{text "\<equiv>"} & @{command assume}~@{text "\<guillemotleft>weak\<hyphen>discharge\<guillemotright> A"} \\
@{command def}~@{text "x \<equiv> a"} & @{text "\<equiv>"} & @{command fix}~@{text x}~@{command assume}~@{text "\<guillemotleft>expansion\<guillemotright> x \<equiv> a"} \\
\end{tabular}
\medskip
@@ -591,14 +591,14 @@
\infer[(@{inference_def discharge})]{@{text "\<strut>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
\]
\[
- \infer[(@{inference_def "weak\<dash>discharge"})]{@{text "\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
+ \infer[(@{inference_def "weak\<hyphen>discharge"})]{@{text "\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
\]
\[
\infer[(@{inference_def expansion})]{@{text "\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a"}}{@{text "\<strut>\<Gamma> \<turnstile> B x"}}
\]
\medskip Note that @{inference discharge} and @{inference
- "weak\<dash>discharge"} differ in the marker for @{prop A}, which is
+ "weak\<hyphen>discharge"} differ in the marker for @{prop A}, which is
relevant when the result of a @{command fix}-@{command
assume}-@{command show} outline is composed with a pending goal,
cf.\ \secref{sec:framework-subproof}.
--- a/doc-src/IsarRef/Thy/document/Framework.tex Tue May 03 21:40:14 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Framework.tex Tue May 03 21:44:05 2011 +0200
@@ -538,7 +538,7 @@
\infer[(\hyperlink{inference.refinement}{\mbox{\isa{refinement}}})]
{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec G{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}{\isaliteral{22}{\isachardoublequote}}}}
{\begin{tabular}{rl}
- \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C646173683E}{\isasymdash}}proof{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
+ \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}proof{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec G\ \isaliteral{5C3C5E7665633E}{}\isactrlvec a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ \isaliteral{5C3C5E7665633E}{}\isactrlvec a{\isaliteral{22}{\isachardoublequote}}} \\
\isa{{\isaliteral{22}{\isachardoublequote}}goal{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{27}{\isacharprime}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequote}}} \\
@@ -550,7 +550,7 @@
\end{tabular}}
\]
- \noindent Here the \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C646173683E}{\isasymdash}}proof{\isaliteral{22}{\isachardoublequote}}} rule stems from the
+ \noindent Here the \isa{{\isaliteral{22}{\isachardoublequote}}sub{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}proof{\isaliteral{22}{\isachardoublequote}}} rule stems from the
main \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} outline of
Isar (cf.\ \secref{sec:framework-subproof}): each assumption
indicated in the text results in a marked premise \isa{{\isaliteral{22}{\isachardoublequote}}G{\isaliteral{22}{\isachardoublequote}}} above.
@@ -580,7 +580,7 @@
\medskip
\begin{tabular}{rcl}
- \isa{{\isaliteral{22}{\isachardoublequote}}theory{\isaliteral{5C3C646173683E}{\isasymdash}}stmt{\isaliteral{22}{\isachardoublequote}}} & = & \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}statement\ proof\ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~~\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]
+ \isa{{\isaliteral{22}{\isachardoublequote}}theory{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}stmt{\isaliteral{22}{\isachardoublequote}}} & = & \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}statement\ proof\ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~~\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]
\isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{22}{\isachardoublequote}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}\ stmt\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]
@@ -687,7 +687,7 @@
\medskip
\begin{tabular}{rcl}
- \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6775696C6C656D6F746C6566743E}{\isasymguillemotleft}}weak{\isaliteral{5C3C646173683E}{\isasymdash}}discharge{\isaliteral{5C3C6775696C6C656D6F7472696768743E}{\isasymguillemotright}}\ A{\isaliteral{22}{\isachardoublequote}}} \\
+ \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6775696C6C656D6F746C6566743E}{\isasymguillemotleft}}weak{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}discharge{\isaliteral{5C3C6775696C6C656D6F7472696768743E}{\isasymguillemotright}}\ A{\isaliteral{22}{\isachardoublequote}}} \\
\hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ a{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6775696C6C656D6F746C6566743E}{\isasymguillemotleft}}expansion{\isaliteral{5C3C6775696C6C656D6F7472696768743E}{\isasymguillemotright}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ a{\isaliteral{22}{\isachardoublequote}}} \\
\end{tabular}
\medskip
@@ -696,13 +696,13 @@
\infer[(\indexdef{}{inference}{discharge}\hypertarget{inference.discharge}{\hyperlink{inference.discharge}{\mbox{\isa{discharge}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{22}{\isachardoublequote}}}}
\]
\[
- \infer[(\indexdef{}{inference}{weak-discharge}\hypertarget{inference.weak-discharge}{\hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C646173683E}{\isasymdash}}discharge}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{22}{\isachardoublequote}}}}
+ \infer[(\indexdef{}{inference}{weak-discharge}\hypertarget{inference.weak-discharge}{\hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}discharge}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{22}{\isachardoublequote}}}}
\]
\[
\infer[(\indexdef{}{inference}{expansion}\hypertarget{inference.expansion}{\hyperlink{inference.expansion}{\mbox{\isa{expansion}}}})]{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ a{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C73747275743E}{\isasymstrut}}{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B\ x{\isaliteral{22}{\isachardoublequote}}}}
\]
- \medskip Note that \hyperlink{inference.discharge}{\mbox{\isa{discharge}}} and \hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C646173683E}{\isasymdash}}discharge}}} differ in the marker for \isa{A}, which is
+ \medskip Note that \hyperlink{inference.discharge}{\mbox{\isa{discharge}}} and \hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}discharge}}} differ in the marker for \isa{A}, which is
relevant when the result of a \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} outline is composed with a pending goal,
cf.\ \secref{sec:framework-subproof}.
--- a/doc-src/IsarRef/style.sty Tue May 03 21:40:14 2011 +0200
+++ b/doc-src/IsarRef/style.sty Tue May 03 21:44:05 2011 +0200
@@ -37,7 +37,6 @@
\parindent 0pt\parskip 0.5ex
\isabellestyle{itunderscore}
-\newcommand{\isasymdash}{\mbox{-}}
\railtermfont{\isabellestyle{tt}}
\railnontermfont{\isabellestyle{itunderscore}}
--- a/doc-src/antiquote_setup.ML Tue May 03 21:40:14 2011 +0200
+++ b/doc-src/antiquote_setup.ML Tue May 03 21:44:05 2011 +0200
@@ -19,7 +19,7 @@
| "{" => "\\{"
| "|" => "$\\mid$"
| "}" => "\\}"
- | "\<dash>" => "-"
+ | "\<hyphen>" => "-"
| c => c);
fun clean_name "\<dots>" = "dots"
@@ -28,7 +28,7 @@
| clean_name "_" = "underscore"
| clean_name "{" = "braceleft"
| clean_name "}" = "braceright"
- | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
+ | clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c);
(* verbatim text *)