# HG changeset patch
# User wenzelm
# Date 1336305485 -7200
# Node ID 1f6f519cdb32c22457dc670c00d44eed79c05840
# Parent  861dc91849204e606f018716cd05b7deb1d3ff8a
tuned proofs;

diff -r 861dc9184920 -r 1f6f519cdb32 src/HOL/Isar_Examples/Group_Context.thy
--- a/src/HOL/Isar_Examples/Group_Context.thy	Sun May 06 13:22:37 2012 +0200
+++ b/src/HOL/Isar_Examples/Group_Context.thy	Sun May 06 13:58:05 2012 +0200
@@ -55,10 +55,10 @@
   finally show "x ** one = x" .
 qed
 
-lemma one_equality: "e ** x = x \<Longrightarrow> one = e"
+lemma one_equality:
+  assumes eq: "e ** x = x"
+  shows "one = e"
 proof -
-  fix e x
-  assume eq: "e ** x = x"
   have "one = x ** inverse x"
     by (simp only: right_inverse)
   also have "\<dots> = (e ** x) ** inverse x"
@@ -72,10 +72,10 @@
   finally show "one = e" .
 qed
 
-lemma inverse_equality: "x' ** x = one \<Longrightarrow> inverse x = x'"
+lemma inverse_equality:
+  assumes eq: "x' ** x = one"
+  shows "inverse x = x'"
 proof -
-  fix x x'
-  assume eq: "x' ** x = one"
   have "inverse x = one ** inverse x"
     by (simp only: left_one)
   also have "\<dots> = (x' ** x) ** inverse x"