remobed obsolete keyword concl;
authorwenzelm
Wed May 14 14:43:34 2008 +0200 (2008-05-14 ago)
changeset 268889942cd184c48
parent 26887 0ae304689d01
child 26889 ccea41fb5c39
remobed obsolete keyword concl;
doc-src/IsarRef/Thy/Proof.thy
src/HOL/Bali/AxSound.thy
src/Pure/Isar/isar_syn.ML
     1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Wed May 14 11:17:36 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Wed May 14 14:43:34 2008 +0200
     1.3 @@ -607,10 +607,10 @@
     1.4    \item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
     1.5    positional instantiation of term variables.  The terms @{text
     1.6    "t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
     1.7 -  variables occurring in a theorem from left to right; ``@{text
     1.8 -  _}'' (underscore) indicates to skip a position.  Arguments following
     1.9 -  a ``@{keyword "concl"}@{text ":"}'' specification refer to positions
    1.10 -  of the conclusion of a rule.
    1.11 +  variables occurring in a theorem from left to right; ``@{text _}''
    1.12 +  (underscore) indicates to skip a position.  Arguments following a
    1.13 +  ``@{text "concl:"}'' specification refer to positions of the
    1.14 +  conclusion of a rule.
    1.15    
    1.16    \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
    1.17    x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic
     2.1 --- a/src/HOL/Bali/AxSound.thy	Wed May 14 11:17:36 2008 +0200
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Wed May 14 14:43:34 2008 +0200
     2.3 @@ -294,7 +294,7 @@
     2.4     and    wt: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T"
     2.5     and    da: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>C"
     2.6     and    elim: "\<lbrakk>Q v s1 Z; s1\<Colon>\<preceq>(G,L)\<rbrakk> \<Longrightarrow> concl" 
     2.7 -  shows "concl"
     2.8 +  shows concl
     2.9  using prems
    2.10  by (simp add: ax_valids2_def triple_valid2_def2) fast
    2.11  (* why consumes 5?. If I want to apply this lemma in a context wgere
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Wed May 14 11:17:36 2008 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed May 14 14:43:34 2008 +0200
     3.3 @@ -20,7 +20,7 @@
     3.4   ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
     3.5    "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
     3.6    "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
     3.7 -  "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
     3.8 +  "advanced", "and", "assumes", "attach", "begin", "binder",
     3.9    "constrains", "defines", "fixes", "for", "identifier", "if",
    3.10    "imports", "in", "includes", "infix", "infixl", "infixr", "is",
    3.11    "notes", "obtains", "open", "output", "overloaded", "shows",