renamed "prems" to "that";
authorwenzelm
Sat Jun 13 13:09:05 2015 +0200 (2015-06-13)
changeset 60449229bad93377e
parent 60448 78f3c67bc35e
child 60450 b54b913dfa6a
renamed "prems" to "that";
NEWS
src/Doc/Isar_Ref/Proof.thy
src/HOL/Isar_Examples/Hoare_Ex.thy
src/HOL/Isar_Examples/Nested_Datatype.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/Pure/Isar/auto_bind.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/proof.ML
     1.1 --- a/NEWS	Thu Jun 11 22:47:53 2015 +0200
     1.2 +++ b/NEWS	Sat Jun 13 13:09:05 2015 +0200
     1.3 @@ -24,13 +24,13 @@
     1.4      for x :: 'a and y :: 'a
     1.5      <proof>
     1.6  
     1.7 -The local assumptions are always bound to the name "prems".  The result
     1.8 -is exported from context of the statement as usual.  The above roughly
     1.9 +The local assumptions are bound to the name "that". The result is
    1.10 +exported from context of the statement as usual. The above roughly
    1.11  corresponds to a raw proof block like this:
    1.12  
    1.13    {
    1.14      fix x :: 'a and y :: 'a
    1.15 -    assume prems: "A x" "B y"
    1.16 +    assume that: "A x" "B y"
    1.17      have "C x y" <proof>
    1.18    }
    1.19    note result = this
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Thu Jun 11 22:47:53 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sat Jun 13 13:09:05 2015 +0200
     2.3 @@ -435,15 +435,13 @@
     2.4       @@{command schematic_corollary}) (stmt | statement)
     2.5      ;
     2.6      (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
     2.7 -      stmt if_prems @{syntax for_fixes}
     2.8 +      stmt (@'if' stmt)? @{syntax for_fixes}
     2.9      ;
    2.10      @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
    2.11      ;
    2.12    
    2.13      stmt: (@{syntax props} + @'and')
    2.14      ;
    2.15 -    if_prems: (@'if' stmt)?
    2.16 -    ;
    2.17      statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
    2.18        conclusion
    2.19      ;
     3.1 --- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Thu Jun 11 22:47:53 2015 +0200
     3.2 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Sat Jun 13 13:09:05 2015 +0200
     3.3 @@ -224,9 +224,9 @@
     3.4    proof hoare
     3.5      show "?inv 0 1" by simp
     3.6      show "?inv (s + i) (i + 1)" if "?inv s i \<and> i \<noteq> n" for s i
     3.7 -      using prems by simp
     3.8 +      using that by simp
     3.9      show "s = ?sum n" if "?inv s i \<and> \<not> i \<noteq> n" for s i
    3.10 -      using prems by simp
    3.11 +      using that by simp
    3.12    qed
    3.13  qed
    3.14  
     4.1 --- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Thu Jun 11 22:47:53 2015 +0200
     4.2 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Sat Jun 13 13:09:05 2015 +0200
     4.3 @@ -39,10 +39,10 @@
     4.4    proof (induct t rule: subst_term.induct)
     4.5      show "?P (Var a)" for a by simp
     4.6      show "?P (App b ts)" if "?Q ts" for b ts
     4.7 -      using prems by (simp only: subst_simps)
     4.8 +      using that by (simp only: subst_simps)
     4.9      show "?Q []" by simp
    4.10      show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
    4.11 -      using prems by (simp only: subst_simps)
    4.12 +      using that by (simp only: subst_simps)
    4.13    qed
    4.14  qed
    4.15  
     5.1 --- a/src/HOL/Library/Convex.thy	Thu Jun 11 22:47:53 2015 +0200
     5.2 +++ b/src/HOL/Library/Convex.thy	Sat Jun 13 13:09:05 2015 +0200
     5.3 @@ -538,7 +538,7 @@
     5.4        by auto
     5.5      let ?a = "\<lambda>j. a j / (1 - a i)"
     5.6      have a_nonneg: "?a j \<ge> 0" if "j \<in> s" for j
     5.7 -      using i0 insert prems by fastforce
     5.8 +      using i0 insert that by fastforce
     5.9      have "(\<Sum> j \<in> insert i s. a j) = 1"
    5.10        using insert by auto
    5.11      then have "(\<Sum> j \<in> s. a j) = 1 - a i"
     6.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Jun 11 22:47:53 2015 +0200
     6.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jun 13 13:09:05 2015 +0200
     6.3 @@ -1191,7 +1191,7 @@
     6.4    shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
     6.5  proof -
     6.6    have False if "h \<noteq> 0" "t = 0" and "pCons a (pCons b p) = pCons h t" for h t
     6.7 -    using l prems by simp
     6.8 +    using l that by simp
     6.9    then have th: "\<not> (\<exists> h t. h \<noteq> 0 \<and> t = 0 \<and> pCons a (pCons b p) = pCons h t)"
    6.10      by blast
    6.11    from fundamental_theorem_of_algebra_alt[OF th] show ?thesis
     7.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jun 11 22:47:53 2015 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Jun 13 13:09:05 2015 +0200
     7.3 @@ -190,10 +190,10 @@
     7.4      using \<open>finite simplices\<close> unfolding F_eq by auto
     7.5  
     7.6    show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
     7.7 -    using bnd prems by auto
     7.8 +    using bnd that by auto
     7.9  
    7.10    show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
    7.11 -    using nbnd prems by auto
    7.12 +    using nbnd that by auto
    7.13  
    7.14    show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
    7.15      using odd_card by simp
     8.1 --- a/src/Pure/Isar/auto_bind.ML	Thu Jun 11 22:47:53 2015 +0200
     8.2 +++ b/src/Pure/Isar/auto_bind.ML	Sat Jun 13 13:09:05 2015 +0200
     8.3 @@ -9,7 +9,6 @@
     8.4    val thesisN: string
     8.5    val thisN: string
     8.6    val thatN: string
     8.7 -  val premsN: string
     8.8    val assmsN: string
     8.9    val abs_params: term -> term -> term
    8.10    val goal: Proof.context -> term list -> (indexname * term option) list
    8.11 @@ -26,7 +25,6 @@
    8.12  val thisN = "this";
    8.13  val thatN = "that";
    8.14  val assmsN = "assms";
    8.15 -val premsN = "prems";
    8.16  
    8.17  fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
    8.18  
     9.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Jun 11 22:47:53 2015 +0200
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jun 13 13:09:05 2015 +0200
     9.3 @@ -491,7 +491,8 @@
     9.4  
     9.5  
     9.6  val structured_statement =
     9.7 -  Parse_Spec.statement -- Parse_Spec.if_prems -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
     9.8 +  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
     9.9 +    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
    9.10  
    9.11  val _ =
    9.12    Outer_Syntax.command @{command_keyword have} "state local goal"
    10.1 --- a/src/Pure/Isar/parse_spec.ML	Thu Jun 11 22:47:53 2015 +0200
    10.2 +++ b/src/Pure/Isar/parse_spec.ML	Sat Jun 13 13:09:05 2015 +0200
    10.3 @@ -24,7 +24,7 @@
    10.4    val locale_expression: bool -> Expression.expression parser
    10.5    val context_element: Element.context parser
    10.6    val statement: (Attrib.binding * (string * string list) list) list parser
    10.7 -  val if_prems: (Attrib.binding * (string * string list) list) list parser
    10.8 +  val if_statement: (Attrib.binding * (string * string list) list) list parser
    10.9    val obtains: Element.obtains parser
   10.10    val general_statement: (Element.context list * Element.statement) parser
   10.11    val statement_keyword: string parser
   10.12 @@ -132,8 +132,7 @@
   10.13  (* statements *)
   10.14  
   10.15  val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
   10.16 -
   10.17 -val if_prems = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
   10.18 +val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
   10.19  
   10.20  val obtain_case =
   10.21    Parse.parbinding --
    11.1 --- a/src/Pure/Isar/proof.ML	Thu Jun 11 22:47:53 2015 +0200
    11.2 +++ b/src/Pure/Isar/proof.ML	Sat Jun 13 13:09:05 2015 +0200
    11.3 @@ -1012,7 +1012,7 @@
    11.4            |> (fn (premss, ctxt') => ctxt'
    11.5                  |> not (null assumes_propss) ?
    11.6                    (snd o Proof_Context.note_thmss ""
    11.7 -                    [((Binding.name Auto_Bind.premsN, []),
    11.8 +                    [((Binding.name Auto_Bind.thatN, []),
    11.9                        [(Assumption.local_prems_of ctxt' ctxt, [])])])
   11.10                  |> (snd o Proof_Context.note_thmss ""
   11.11                      (assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));