author wenzelm Sat Jun 13 13:09:05 2015 +0200 (2015-06-13) changeset 60449 229bad93377e parent 60448 78f3c67bc35e child 60450 b54b913dfa6a
renamed "prems" to "that";
 NEWS file | annotate | diff | revisions src/Doc/Isar_Ref/Proof.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Hoare_Ex.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Nested_Datatype.thy file | annotate | diff | revisions src/HOL/Library/Convex.thy file | annotate | diff | revisions src/HOL/Library/Fundamental_Theorem_Algebra.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy file | annotate | diff | revisions src/Pure/Isar/auto_bind.ML file | annotate | diff | revisions src/Pure/Isar/isar_syn.ML file | annotate | diff | revisions src/Pure/Isar/parse_spec.ML file | annotate | diff | revisions src/Pure/Isar/proof.ML file | annotate | diff | revisions
```     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)));
```