# HG changeset patch
# User wenzelm
# Date 1210769014 -7200
# Node ID 9942cd184c4820531a5a9bb49233e8402ea1a7df
# Parent  0ae304689d018c561a4f5d99f57d07553a744a86
remobed obsolete keyword concl;

diff -r 0ae304689d01 -r 9942cd184c48 doc-src/IsarRef/Thy/Proof.thy
--- 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
diff -r 0ae304689d01 -r 9942cd184c48 src/HOL/Bali/AxSound.thy
--- 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
diff -r 0ae304689d01 -r 9942cd184c48 src/Pure/Isar/isar_syn.ML
--- 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",