--- a/NEWS Thu Jun 11 22:47:53 2015 +0200
+++ b/NEWS Sat Jun 13 13:09:05 2015 +0200
@@ -24,13 +24,13 @@
for x :: 'a and y :: 'a
<proof>
-The local assumptions are always bound to the name "prems". The result
-is exported from context of the statement as usual. The above roughly
+The local assumptions are bound to the name "that". The result is
+exported from context of the statement as usual. The above roughly
corresponds to a raw proof block like this:
{
fix x :: 'a and y :: 'a
- assume prems: "A x" "B y"
+ assume that: "A x" "B y"
have "C x y" <proof>
}
note result = this
--- a/src/Doc/Isar_Ref/Proof.thy Thu Jun 11 22:47:53 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Sat Jun 13 13:09:05 2015 +0200
@@ -435,15 +435,13 @@
@@{command schematic_corollary}) (stmt | statement)
;
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
- stmt if_prems @{syntax for_fixes}
+ stmt (@'if' stmt)? @{syntax for_fixes}
;
@@{command print_statement} @{syntax modes}? @{syntax thmrefs}
;
stmt: (@{syntax props} + @'and')
;
- if_prems: (@'if' stmt)?
- ;
statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
conclusion
;
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Thu Jun 11 22:47:53 2015 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Sat Jun 13 13:09:05 2015 +0200
@@ -224,9 +224,9 @@
proof hoare
show "?inv 0 1" by simp
show "?inv (s + i) (i + 1)" if "?inv s i \<and> i \<noteq> n" for s i
- using prems by simp
+ using that by simp
show "s = ?sum n" if "?inv s i \<and> \<not> i \<noteq> n" for s i
- using prems by simp
+ using that by simp
qed
qed
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Thu Jun 11 22:47:53 2015 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Sat Jun 13 13:09:05 2015 +0200
@@ -39,10 +39,10 @@
proof (induct t rule: subst_term.induct)
show "?P (Var a)" for a by simp
show "?P (App b ts)" if "?Q ts" for b ts
- using prems by (simp only: subst_simps)
+ using that by (simp only: subst_simps)
show "?Q []" by simp
show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
- using prems by (simp only: subst_simps)
+ using that by (simp only: subst_simps)
qed
qed
--- a/src/HOL/Library/Convex.thy Thu Jun 11 22:47:53 2015 +0200
+++ b/src/HOL/Library/Convex.thy Sat Jun 13 13:09:05 2015 +0200
@@ -538,7 +538,7 @@
by auto
let ?a = "\<lambda>j. a j / (1 - a i)"
have a_nonneg: "?a j \<ge> 0" if "j \<in> s" for j
- using i0 insert prems by fastforce
+ using i0 insert that by fastforce
have "(\<Sum> j \<in> insert i s. a j) = 1"
using insert by auto
then have "(\<Sum> j \<in> s. a j) = 1 - a i"
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Thu Jun 11 22:47:53 2015 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sat Jun 13 13:09:05 2015 +0200
@@ -1191,7 +1191,7 @@
shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
proof -
have False if "h \<noteq> 0" "t = 0" and "pCons a (pCons b p) = pCons h t" for h t
- using l prems by simp
+ using l that by simp
then have th: "\<not> (\<exists> h t. h \<noteq> 0 \<and> t = 0 \<and> pCons a (pCons b p) = pCons h t)"
by blast
from fundamental_theorem_of_algebra_alt[OF th] show ?thesis
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Jun 11 22:47:53 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sat Jun 13 13:09:05 2015 +0200
@@ -190,10 +190,10 @@
using \<open>finite simplices\<close> unfolding F_eq by auto
show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
- using bnd prems by auto
+ using bnd that by auto
show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
- using nbnd prems by auto
+ using nbnd that by auto
show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
using odd_card by simp
--- a/src/Pure/Isar/auto_bind.ML Thu Jun 11 22:47:53 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML Sat Jun 13 13:09:05 2015 +0200
@@ -9,7 +9,6 @@
val thesisN: string
val thisN: string
val thatN: string
- val premsN: string
val assmsN: string
val abs_params: term -> term -> term
val goal: Proof.context -> term list -> (indexname * term option) list
@@ -26,7 +25,6 @@
val thisN = "this";
val thatN = "that";
val assmsN = "assms";
-val premsN = "prems";
fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
--- a/src/Pure/Isar/isar_syn.ML Thu Jun 11 22:47:53 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sat Jun 13 13:09:05 2015 +0200
@@ -491,7 +491,8 @@
val structured_statement =
- Parse_Spec.statement -- Parse_Spec.if_prems -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
+ Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
+ >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
val _ =
Outer_Syntax.command @{command_keyword have} "state local goal"
--- a/src/Pure/Isar/parse_spec.ML Thu Jun 11 22:47:53 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML Sat Jun 13 13:09:05 2015 +0200
@@ -24,7 +24,7 @@
val locale_expression: bool -> Expression.expression parser
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
- val if_prems: (Attrib.binding * (string * string list) list) list parser
+ val if_statement: (Attrib.binding * (string * string list) list) list parser
val obtains: Element.obtains parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
@@ -132,8 +132,7 @@
(* statements *)
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
-
-val if_prems = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
+val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
val obtain_case =
Parse.parbinding --
--- a/src/Pure/Isar/proof.ML Thu Jun 11 22:47:53 2015 +0200
+++ b/src/Pure/Isar/proof.ML Sat Jun 13 13:09:05 2015 +0200
@@ -1012,7 +1012,7 @@
|> (fn (premss, ctxt') => ctxt'
|> not (null assumes_propss) ?
(snd o Proof_Context.note_thmss ""
- [((Binding.name Auto_Bind.premsN, []),
+ [((Binding.name Auto_Bind.thatN, []),
[(Assumption.local_prems_of ctxt' ctxt, [])])])
|> (snd o Proof_Context.note_thmss ""
(assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));