--- a/doc-src/IsarRef/Thy/Proof.thy Wed May 14 11:17:36 2008 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Wed May 14 14:43:34 2008 +0200
@@ -607,10 +607,10 @@
\item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
positional instantiation of term variables. The terms @{text
"t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
- variables occurring in a theorem from left to right; ``@{text
- _}'' (underscore) indicates to skip a position. Arguments following
- a ``@{keyword "concl"}@{text ":"}'' specification refer to positions
- of the conclusion of a rule.
+ variables occurring in a theorem from left to right; ``@{text _}''
+ (underscore) indicates to skip a position. Arguments following a
+ ``@{text "concl:"}'' specification refer to positions of the
+ conclusion of a rule.
\item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic
--- a/src/HOL/Bali/AxSound.thy Wed May 14 11:17:36 2008 +0200
+++ b/src/HOL/Bali/AxSound.thy Wed May 14 14:43:34 2008 +0200
@@ -294,7 +294,7 @@
and wt: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T"
and da: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>C"
and elim: "\<lbrakk>Q v s1 Z; s1\<Colon>\<preceq>(G,L)\<rbrakk> \<Longrightarrow> concl"
- shows "concl"
+ shows concl
using prems
by (simp add: ax_valids2_def triple_valid2_def2) fast
(* why consumes 5?. If I want to apply this lemma in a context wgere
--- a/src/Pure/Isar/isar_syn.ML Wed May 14 11:17:36 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed May 14 14:43:34 2008 +0200
@@ -20,7 +20,7 @@
["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
"=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
"\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
- "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
+ "advanced", "and", "assumes", "attach", "begin", "binder",
"constrains", "defines", "fixes", "for", "identifier", "if",
"imports", "in", "includes", "infix", "infixl", "infixr", "is",
"notes", "obtains", "open", "output", "overloaded", "shows",