--- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Jan 25 21:14:00 2012 +0100
@@ -356,7 +356,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type term} \\
- @{index_ML "op aconv": "term * term -> bool"} \\
+ @{index_ML_op "aconv": "term * term -> bool"} \\
@{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
@{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
@{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
@@ -380,7 +380,7 @@
\item Type @{ML_type term} represents de-Bruijn terms, with comments
in abstractions, and explicitly named free variables and constants;
this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
- Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.
+ Var}, @{ML Const}, @{ML Abs}, @{ML_op "$"}.
\item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text
"\<alpha>"}-equivalence of two terms. This is the basic equality relation
@@ -700,7 +700,7 @@
\item @{ML Thm.capply}, @{ML Thm.cabs}, @{ML Thm.all}, @{ML
Drule.mk_implies} etc.\ compose certified terms (or propositions)
incrementally. This is equivalent to @{ML Thm.cterm_of} after
- unchecked @{ML "op $"}, @{ML lambda}, @{ML Logic.all}, @{ML
+ unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML
Logic.mk_implies} etc., but there can be a big difference in
performance when large existing entities are composed by a few extra
constructions on top. There are separate operations to decompose
@@ -1084,14 +1084,14 @@
text %mlref {*
\begin{mldecls}
- @{index_ML "op RSN": "thm * (int * thm) -> thm"} \\
- @{index_ML "op RS": "thm * thm -> thm"} \\
+ @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\
+ @{index_ML_op "RS": "thm * thm -> thm"} \\
- @{index_ML "op RLN": "thm list * (int * thm list) -> thm list"} \\
- @{index_ML "op RL": "thm list * thm list -> thm list"} \\
+ @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\
+ @{index_ML_op "RL": "thm list * thm list -> thm list"} \\
- @{index_ML "op MRS": "thm list * thm -> thm"} \\
- @{index_ML "op OF": "thm * thm list -> thm"} \\
+ @{index_ML_op "MRS": "thm list * thm -> thm"} \\
+ @{index_ML_op "OF": "thm * thm list -> thm"} \\
\end{mldecls}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 25 21:14:00 2012 +0100
@@ -849,10 +849,10 @@
text %mlref {*
\begin{mldecls}
- @{index_ML "op |> ": "'a * ('a -> 'b) -> 'b"} \\
- @{index_ML "op |-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
- @{index_ML "op #> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
- @{index_ML "op #-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
+ @{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\
+ @{index_ML_op "|-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
+ @{index_ML_op "#> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
+ @{index_ML_op "#-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
\end{mldecls}
%FIXME description!?
@@ -1465,7 +1465,7 @@
@{index_ML_type "'a Unsynchronized.ref"} \\
@{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
@{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\
- @{index_ML "op :=": "'a Unsynchronized.ref * 'a -> unit"} \\
+ @{index_ML_op ":=": "'a Unsynchronized.ref * 'a -> unit"} \\
\end{mldecls}
*}
@@ -1477,7 +1477,7 @@
The unwieldy name of @{ML Unsynchronized.ref} for the constructor
for references in Isabelle/ML emphasizes the inconveniences caused by
- mutability. Existing operations @{ML "!"} and @{ML "op :="} are
+ mutability. Existing operations @{ML "!"} and @{ML_op ":="} are
unchanged, but should be used with special precautions, say in a
strictly local situation that is guaranteed to be restricted to
sequential evaluation --- now and in the future.
--- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 21:14:00 2012 +0100
@@ -414,22 +414,23 @@
text {* Sequential composition and alternative choices are the most
basic ways to combine tactics, similarly to ``@{verbatim ","}'' and
``@{verbatim "|"}'' in Isar method notation. This corresponds to
- @{text "THEN"} and @{text "ORELSE"} in ML, but there are further
- possibilities for fine-tuning alternation of tactics such as @{text
+ @{ML_op "THEN"} and @{ML_op "ORELSE"} in ML, but there are further
+ possibilities for fine-tuning alternation of tactics such as @{ML_op
"APPEND"}. Further details become visible in ML due to explicit
- subgoal addressing. *}
+ subgoal addressing.
+*}
text %mlref {*
\begin{mldecls}
- @{index_ML "op THEN": "tactic * tactic -> tactic"} \\
- @{index_ML "op ORELSE": "tactic * tactic -> tactic"} \\
- @{index_ML "op APPEND": "tactic * tactic -> tactic"} \\
+ @{index_ML_op "THEN": "tactic * tactic -> tactic"} \\
+ @{index_ML_op "ORELSE": "tactic * tactic -> tactic"} \\
+ @{index_ML_op "APPEND": "tactic * tactic -> tactic"} \\
@{index_ML "EVERY": "tactic list -> tactic"} \\
@{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
- @{index_ML "op THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
- @{index_ML "op ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
- @{index_ML "op APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+ @{index_ML_op "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+ @{index_ML_op "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+ @{index_ML_op "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
@{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
@{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
@{index_ML "EVERY1": "(int -> tactic) list -> tactic"} \\
@@ -438,47 +439,50 @@
\begin{description}
- \item @{text "tac\<^sub>1 THEN tac\<^sub>2"} is the sequential composition of
- @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a proof state, it
- returns all states reachable in two steps by applying @{text "tac\<^sub>1"}
- followed by @{text "tac\<^sub>2"}. First, it applies @{text "tac\<^sub>1"} to the
- proof state, getting a sequence of possible next states; then, it
- applies @{text "tac\<^sub>2"} to each of these and concatenates the results
- to produce again one flat sequence of states.
+ \item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential
+ composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a
+ proof state, it returns all states reachable in two steps by
+ applying @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}. First, it
+ applies @{text "tac\<^sub>1"} to the proof state, getting a sequence of
+ possible next states; then, it applies @{text "tac\<^sub>2"} to each of
+ these and concatenates the results to produce again one flat
+ sequence of states.
- \item @{text "tac\<^sub>1 ORELSE tac\<^sub>2"} makes a choice between @{text
- "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it tries @{text
- "tac\<^sub>1"} and returns the result if non-empty; if @{text "tac\<^sub>1"} fails
- then it uses @{text "tac\<^sub>2"}. This is a deterministic choice: if
- @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded from the
- result.
+ \item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice
+ between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it
+ tries @{text "tac\<^sub>1"} and returns the result if non-empty; if @{text
+ "tac\<^sub>1"} fails then it uses @{text "tac\<^sub>2"}. This is a deterministic
+ choice: if @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded
+ from the result.
- \item @{text "tac\<^sub>1 APPEND tac\<^sub>2"} concatenates the possible results
- of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike @{text "ORELSE"} there
- is \emph{no commitment} to either tactic, so @{text "APPEND"} helps
- to avoid incompleteness during search, at the cost of potential
- inefficiencies.
+ \item @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the
+ possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike
+ @{ML_op "ORELSE"} there is \emph{no commitment} to either tactic, so
+ @{ML_op "APPEND"} helps to avoid incompleteness during search, at
+ the cost of potential inefficiencies.
- \item @{text "EVERY [tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1 THEN
- \<dots> THEN tac\<^sub>n"}. Note that @{text "EVERY []"} is the same as @{ML
- all_tac}: it always succeeds.
+ \item @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
+ "tac\<^sub>1"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac\<^sub>n"}.
+ Note that @{ML "EVERY []"} is the same as @{ML all_tac}: it always
+ succeeds.
- \item @{text "FIRST [tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1
- ORELSE \<dots> ORELSE tac\<^sub>n"}. Note that @{text "FIRST []"} is the same as
- @{ML no_tac}: it always fails.
+ \item @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
+ "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op "ORELSE"}~@{text
+ "tac\<^sub>n"}. Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it
+ always fails.
- \item @{text "THEN'"}, @{text "ORELSE'"}, and @{text "APPEND'"} are
- lifted versions of @{text "THEN"}, @{text "ORELSE"}, and @{text
- "APPEND"}, for tactics with explicit subgoal addressing. This means
- @{text "(tac\<^sub>1 THEN' tac\<^sub>2) i"} is the same as @{text "(tac\<^sub>1 i THEN
- tac\<^sub>2 i)"} etc.
+ \item @{ML_op "THEN'"}, @{ML_op "ORELSE'"}, and @{ML_op "APPEND'"}
+ are lifted versions of @{ML_op "THEN"}, @{ML_op "ORELSE"}, and
+ @{ML_op "APPEND"}, for tactics with explicit subgoal addressing.
+ This means @{text "(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the
+ same as @{text "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"} etc.
- \item @{text "EVERY'"} and @{text "FIRST'"} are lifted versions of
- @{text "EVERY'"} and @{text "FIRST'"}, for tactics with explicit
- subgoal addressing.
+ \item @{ML "EVERY'"} and @{ML "FIRST'"} are lifted versions of @{ML
+ "EVERY'"} and @{ML "FIRST'"}, for tactics with explicit subgoal
+ addressing.
- \item @{text "EVERY1"} and @{text "FIRST1"} are convenience versions
- of @{text "EVERY'"} and @{text "FIRST'"}, applied to subgoal 1.
+ \item @{ML "EVERY1"} and @{ML "FIRST1"} are convenience versions of
+ @{ML "EVERY'"} and @{ML "FIRST'"}, applied to subgoal 1.
\end{description}
*}
@@ -543,13 +547,13 @@
\begin{itemize}
- \item @{ML all_tac} is the identity element of the tactical
- @{ML "op THEN"}.
+ \item @{ML all_tac} is the identity element of the tactical @{ML_op
+ "THEN"}.
- \item @{ML no_tac} is the identity element of @{ML "op ORELSE"} and
- @{ML "op APPEND"}. Also, it is a zero element for @{ML "op THEN"},
- which means that @{text "tac THEN"}~@{ML no_tac} is equivalent to
- @{ML no_tac}.
+ \item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and
+ @{ML_op "APPEND"}. Also, it is a zero element for @{ML_op "THEN"},
+ which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is
+ equivalent to @{ML no_tac}.
\item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)
functions over more basic combinators (ignoring some internal
@@ -564,8 +568,8 @@
*}
text {* If @{text "tac"} can return multiple outcomes then so can @{ML
- REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML "op ORELSE"} and not
- @{ML "op APPEND"}, it applies @{text "tac"} as many times as
+ REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML_op "ORELSE"} and not
+ @{ML_op "APPEND"}, it applies @{text "tac"} as many times as
possible in each outcome.
\begin{warn}
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Jan 25 21:14:00 2012 +0100
@@ -394,7 +394,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{term}\verb|type term| \\
- \indexdef{}{ML}{aconv}\verb|op aconv: term * term -> bool| \\
+ \indexdef{}{ML infix}{aconv}\verb|infix aconv: term * term -> bool| \\
\indexdef{}{ML}{Term.map\_types}\verb|Term.map_types: (typ -> typ) -> term -> term| \\
\indexdef{}{ML}{Term.fold\_types}\verb|Term.fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
\indexdef{}{ML}{Term.map\_aterms}\verb|Term.map_aterms: (term -> term) -> term -> term| \\
@@ -417,7 +417,7 @@
\item Type \verb|term| represents de-Bruijn terms, with comments
in abstractions, and explicitly named free variables and constants;
- this is a datatype with constructors \verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|, \verb|Abs|, \verb|op $|.
+ this is a datatype with constructors \verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|, \verb|Abs|, \verb|$|.
\item \isa{t}~\verb|aconv|~\isa{u} checks \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-equivalence of two terms. This is the basic equality relation
on type \verb|term|; raw datatype equality should only be used
@@ -769,7 +769,7 @@
\item \verb|Thm.capply|, \verb|Thm.cabs|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions)
incrementally. This is equivalent to \verb|Thm.cterm_of| after
- unchecked \verb|op $|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in
+ unchecked \verb|$|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in
performance when large existing entities are composed by a few extra
constructions on top. There are separate operations to decompose
certified terms and theorems to produce certified terms again.
@@ -1226,14 +1226,14 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{RSN}\verb|op RSN: thm * (int * thm) -> thm| \\
- \indexdef{}{ML}{RS}\verb|op RS: thm * thm -> thm| \\
+ \indexdef{}{ML infix}{RSN}\verb|infix RSN: thm * (int * thm) -> thm| \\
+ \indexdef{}{ML infix}{RS}\verb|infix RS: thm * thm -> thm| \\
- \indexdef{}{ML}{RLN}\verb|op RLN: thm list * (int * thm list) -> thm list| \\
- \indexdef{}{ML}{RL}\verb|op RL: thm list * thm list -> thm list| \\
+ \indexdef{}{ML infix}{RLN}\verb|infix RLN: thm list * (int * thm list) -> thm list| \\
+ \indexdef{}{ML infix}{RL}\verb|infix RL: thm list * thm list -> thm list| \\
- \indexdef{}{ML}{MRS}\verb|op MRS: thm list * thm -> thm| \\
- \indexdef{}{ML}{OF}\verb|op OF: thm * thm list -> thm| \\
+ \indexdef{}{ML infix}{MRS}\verb|infix MRS: thm list * thm -> thm| \\
+ \indexdef{}{ML infix}{OF}\verb|infix OF: thm * thm list -> thm| \\
\end{mldecls}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 25 21:14:00 2012 +0100
@@ -1076,10 +1076,10 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{$\mid$$>$}\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
- \indexdef{}{ML}{$\mid$-$>$}\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
- \indexdef{}{ML}{\#$>$}\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
- \indexdef{}{ML}{\#-$>$}\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
+ \indexdef{}{ML infix}{$\mid$$>$}\verb|infix |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
+ \indexdef{}{ML infix}{$\mid$-$>$}\verb|infix |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
+ \indexdef{}{ML infix}{\#$>$}\verb|infix #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
+ \indexdef{}{ML infix}{\#-$>$}\verb|infix #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
\end{mldecls}
%FIXME description!?%
@@ -1968,7 +1968,7 @@
\indexdef{}{ML type}{Unsynchronized.ref}\verb|type 'a Unsynchronized.ref| \\
\indexdef{}{ML}{Unsynchronized.ref}\verb|Unsynchronized.ref: 'a -> 'a Unsynchronized.ref| \\
\indexdef{}{ML}{!}\verb|! : 'a Unsynchronized.ref -> 'a| \\
- \indexdef{}{ML}{:=}\verb|op := : 'a Unsynchronized.ref * 'a -> unit| \\
+ \indexdef{}{ML infix}{:=}\verb|infix := : 'a Unsynchronized.ref * 'a -> unit| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1989,7 +1989,7 @@
The unwieldy name of \verb|Unsynchronized.ref| for the constructor
for references in Isabelle/ML emphasizes the inconveniences caused by
- mutability. Existing operations \verb|!| and \verb|op :=| are
+ mutability. Existing operations \verb|!| and \verb|:=| are
unchanged, but should be used with special precautions, say in a
strictly local situation that is guaranteed to be restricted to
sequential evaluation --- now and in the future.
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 21:14:00 2012 +0100
@@ -495,8 +495,8 @@
Sequential composition and alternative choices are the most
basic ways to combine tactics, similarly to ``\verb|,|'' and
``\verb||\verb,|,\verb||'' in Isar method notation. This corresponds to
- \isa{THEN} and \isa{ORELSE} in ML, but there are further
- possibilities for fine-tuning alternation of tactics such as \isa{APPEND}. Further details become visible in ML due to explicit
+ \verb|THEN| and \verb|ORELSE| in ML, but there are further
+ possibilities for fine-tuning alternation of tactics such as \verb|APPEND|. Further details become visible in ML due to explicit
subgoal addressing.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -509,15 +509,15 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{THEN}\verb|op THEN: tactic * tactic -> tactic| \\
- \indexdef{}{ML}{ORELSE}\verb|op ORELSE: tactic * tactic -> tactic| \\
- \indexdef{}{ML}{APPEND}\verb|op APPEND: tactic * tactic -> tactic| \\
+ \indexdef{}{ML infix}{THEN}\verb|infix THEN: tactic * tactic -> tactic| \\
+ \indexdef{}{ML infix}{ORELSE}\verb|infix ORELSE: tactic * tactic -> tactic| \\
+ \indexdef{}{ML infix}{APPEND}\verb|infix APPEND: tactic * tactic -> tactic| \\
\indexdef{}{ML}{EVERY}\verb|EVERY: tactic list -> tactic| \\
\indexdef{}{ML}{FIRST}\verb|FIRST: tactic list -> tactic| \\[0.5ex]
- \indexdef{}{ML}{THEN'}\verb|op THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
- \indexdef{}{ML}{ORELSE'}\verb|op ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
- \indexdef{}{ML}{APPEND'}\verb|op APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
+ \indexdef{}{ML infix}{THEN'}\verb|infix THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
+ \indexdef{}{ML infix}{ORELSE'}\verb|infix ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
+ \indexdef{}{ML infix}{APPEND'}\verb|infix APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
\indexdef{}{ML}{EVERY'}\verb|EVERY': ('a -> tactic) list -> 'a -> tactic| \\
\indexdef{}{ML}{FIRST'}\verb|FIRST': ('a -> tactic) list -> 'a -> tactic| \\
\indexdef{}{ML}{EVERY1}\verb|EVERY1: (int -> tactic) list -> tactic| \\
@@ -526,40 +526,45 @@
\begin{description}
- \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential composition of
- \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a proof state, it
- returns all states reachable in two steps by applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}
- followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the
- proof state, getting a sequence of possible next states; then, it
- applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and concatenates the results
- to produce again one flat sequence of states.
+ \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential
+ composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a
+ proof state, it returns all states reachable in two steps by
+ applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it
+ applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the proof state, getting a sequence of
+ possible next states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of
+ these and concatenates the results to produce again one flat
+ sequence of states.
- \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ ORELSE\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a state, it tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if non-empty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails
- then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. This is a deterministic choice: if
- \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} succeeds then \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is excluded from the
- result.
+ \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice
+ between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a state, it
+ tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if non-empty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. This is a deterministic
+ choice: if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} succeeds then \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is excluded
+ from the result.
- \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ APPEND\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} concatenates the possible results
- of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Unlike \isa{ORELSE} there
- is \emph{no commitment} to either tactic, so \isa{APPEND} helps
- to avoid incompleteness during search, at the cost of potential
- inefficiencies.
+ \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|APPEND|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} concatenates the
+ possible results of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Unlike
+ \verb|ORELSE| there is \emph{no commitment} to either tactic, so
+ \verb|APPEND| helps to avoid incompleteness during search, at
+ the cost of potential inefficiencies.
- \item \isa{EVERY\ {\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \isa{EVERY\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is the same as \verb|all_tac|: it always succeeds.
-
- \item \isa{FIRST\ {\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ ORELSE\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ ORELSE\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \isa{FIRST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is the same as
- \verb|no_tac|: it always fails.
+ \item \verb|EVERY|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}.
+ Note that \verb|EVERY []| is the same as \verb|all_tac|: it always
+ succeeds.
- \item \isa{THEN{\isaliteral{27}{\isacharprime}}}, \isa{ORELSE{\isaliteral{27}{\isacharprime}}}, and \isa{APPEND{\isaliteral{27}{\isacharprime}}} are
- lifted versions of \isa{THEN}, \isa{ORELSE}, and \isa{APPEND}, for tactics with explicit subgoal addressing. This means
- \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN{\isaliteral{27}{\isacharprime}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}} etc.
+ \item \verb|FIRST|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \verb|FIRST []| is the same as \verb|no_tac|: it
+ always fails.
- \item \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}} are lifted versions of
- \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}}, for tactics with explicit
- subgoal addressing.
+ \item \verb|THEN'|, \verb|ORELSE'|, and \verb|APPEND'|
+ are lifted versions of \verb|THEN|, \verb|ORELSE|, and
+ \verb|APPEND|, for tactics with explicit subgoal addressing.
+ This means \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN'|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the
+ same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}} etc.
- \item \isa{EVERY{\isadigit{1}}} and \isa{FIRST{\isadigit{1}}} are convenience versions
- of \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}}, applied to subgoal 1.
+ \item \verb|EVERY'| and \verb|FIRST'| are lifted versions of \verb|EVERY'| and \verb|FIRST'|, for tactics with explicit subgoal
+ addressing.
+
+ \item \verb|EVERY1| and \verb|FIRST1| are convenience versions of
+ \verb|EVERY'| and \verb|FIRST'|, applied to subgoal 1.
\end{description}%
\end{isamarkuptext}%
@@ -654,13 +659,12 @@
\begin{itemize}
- \item \verb|all_tac| is the identity element of the tactical
- \verb|op THEN|.
+ \item \verb|all_tac| is the identity element of the tactical \verb|THEN|.
- \item \verb|no_tac| is the identity element of \verb|op ORELSE| and
- \verb|op APPEND|. Also, it is a zero element for \verb|op THEN|,
- which means that \isa{tac\ THEN}~\verb|no_tac| is equivalent to
- \verb|no_tac|.
+ \item \verb|no_tac| is the identity element of \verb|ORELSE| and
+ \verb|APPEND|. Also, it is a zero element for \verb|THEN|,
+ which means that \isa{tac}~\verb|THEN|~\verb|no_tac| is
+ equivalent to \verb|no_tac|.
\item \verb|TRY| and \verb|REPEAT| can be expressed as (recursive)
functions over more basic combinators (ignoring some internal
@@ -695,8 +699,8 @@
\endisadelimML
%
\begin{isamarkuptext}%
-If \isa{tac} can return multiple outcomes then so can \verb|REPEAT|~\isa{tac}. \verb|REPEAT| uses \verb|op ORELSE| and not
- \verb|op APPEND|, it applies \isa{tac} as many times as
+If \isa{tac} can return multiple outcomes then so can \verb|REPEAT|~\isa{tac}. \verb|REPEAT| uses \verb|ORELSE| and not
+ \verb|APPEND|, it applies \isa{tac} as many times as
possible in each outcome.
\begin{warn}
--- a/doc-src/IsarRef/Thy/Generic.thy Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Wed Jan 25 21:14:00 2012 +0100
@@ -160,8 +160,8 @@
compose rules by resolution. @{attribute THEN} resolves with the
first premise of @{text a} (an alternative position may be also
specified); the @{attribute COMP} version skips the automatic
- lifting process that is normally intended (cf.\ @{ML "op RS"} and
- @{ML "op COMP"} in \cite{isabelle-implementation}).
+ lifting process that is normally intended (cf.\ @{ML_op "RS"} and
+ @{ML_op "COMP"} in \cite{isabelle-implementation}).
\item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
--- a/doc-src/IsarRef/Thy/Proof.thy Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy Wed Jan 25 21:14:00 2012 +0100
@@ -790,7 +790,7 @@
\item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some
theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
- (in parallel). This corresponds to the @{ML "op MRS"} operation in
+ (in parallel). This corresponds to the @{ML_op "MRS"} operation in
ML, but note the reversed order. Positions may be effectively
skipped by including ``@{text _}'' (underscore) as argument.
--- a/doc-src/IsarRef/Thy/document/Generic.tex Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Wed Jan 25 21:14:00 2012 +0100
@@ -277,8 +277,8 @@
compose rules by resolution. \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the
first premise of \isa{a} (an alternative position may be also
specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
- lifting process that is normally intended (cf.\ \verb|op RS| and
- \verb|op COMP| in \cite{isabelle-implementation}).
+ lifting process that is normally intended (cf.\ \verb|RS| and
+ \verb|COMP| in \cite{isabelle-implementation}).
\item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} expand and fold back again the given
definitions throughout a rule.
--- a/doc-src/IsarRef/Thy/document/Proof.tex Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Wed Jan 25 21:14:00 2012 +0100
@@ -1113,7 +1113,7 @@
\item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some
theorem to all of the given rules \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}
- (in parallel). This corresponds to the \verb|op MRS| operation in
+ (in parallel). This corresponds to the \verb|MRS| operation in
ML, but note the reversed order. Positions may be effectively
skipped by including ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'' (underscore) as argument.