src/HOL/ex/Locales.thy

   context elements (parameters, assumptions, etc.) in a casual manner;
   these are discharged when the proof is finished.
 *}
 
 theorem (in group_context)
-  (assumes eq: "e \<cdot> x = x")
-  one_equality: "\<one> = e"
+  assumes eq: "e \<cdot> x = x"
+  shows one_equality: "\<one> = e"
 proof -
   have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
   also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
   also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
   also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)
   also have "\<dots> = e" by (simp only: right_one)
   finally show ?thesis .
 qed
 
 theorem (in group_context)
-  (assumes eq: "x' \<cdot> x = \<one>")
-  inv_equality: "x\<inv> = x'"
+  assumes eq: "x' \<cdot> x = \<one>"
+  shows inv_equality: "x\<inv> = x'"
 proof -
   have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
   also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
   also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
   also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)

 proof (rule inv_equality)
   show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
 qed
 
 theorem (in group_context)
-  (assumes eq: "x\<inv> = y\<inv>")
-  inv_inject: "x = y"
+  assumes eq: "x\<inv> = y\<inv>"
+  shows inv_inject: "x = y"
 proof -
   have "x = x \<cdot> \<one>" by (simp only: right_one)
   also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
   also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)
   also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)

   The following synthetic example demonstrates how to refer to several
   structures of type @{text group} succinctly.  We work with two
   versions of the @{text group} locale above.
 *}
 
-lemma (uses group G + group H)
-  "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
+lemma
+  uses group G + group H
+  shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
   "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and
   "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+
 
 text {*
   Note that the trivial statements above need to be given as a