Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/AxClasses/Group/Group.ML
changeset 5069 3ea049f7979d
parent 3821 151d49052228 
--- a/src/HOL/AxClasses/Group/Group.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/AxClasses/Group/Group.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -9,7 +9,7 @@
 fun ssub r = standard (r RS ssubst);
 
 
-goal thy "x * inverse x = (1::'a::group)";
+Goal "x * inverse x = (1::'a::group)";
 by (rtac (sub left_unit) 1);
 back();
 by (rtac (sub assoc) 1);
@@ -26,7 +26,7 @@
 qed "right_inverse";
 
 
-goal thy "x * 1 = (x::'a::group)";
+Goal "x * 1 = (x::'a::group)";
 by (rtac (sub left_inverse) 1);
 by (rtac (sub assoc) 1);
 by (rtac (ssub right_inverse) 1);
@@ -35,7 +35,7 @@
 qed "right_unit";
 
 
-goal thy "e * x = x --> e = (1::'a::group)";
+Goal "e * x = x --> e = (1::'a::group)";
 by (rtac impI 1);
 by (rtac (sub right_unit) 1);
 back();
@@ -47,7 +47,7 @@
 qed "strong_one_unit";
 
 
-goal thy "EX! e. ALL x. e * x = (x::'a::group)";
+Goal "EX! e. ALL x. e * x = (x::'a::group)";
 by (rtac ex1I 1);
 by (rtac allI 1);
 by (rtac left_unit 1);
@@ -58,7 +58,7 @@
 qed "ex1_unit";
 
 
-goal thy "ALL x. EX! e. e * x = (x::'a::group)";
+Goal "ALL x. EX! e. e * x = (x::'a::group)";
 by (rtac allI 1);
 by (rtac ex1I 1);
 by (rtac left_unit 1);
@@ -67,7 +67,7 @@
 qed "ex1_unit'";
 
 
-goal thy "inj (op * (x::'a::group))";
+Goal "inj (op * (x::'a::group))";
 by (rtac injI 1);
 by (rtac (sub left_unit) 1);
 back();
@@ -82,7 +82,7 @@
 qed "inj_times";
 
 
-goal thy "y * x = 1 --> y = inverse (x::'a::group)";
+Goal "y * x = 1 --> y = inverse (x::'a::group)";
 by (rtac impI 1);
 by (rtac (sub right_unit) 1);
 back();
@@ -98,7 +98,7 @@
 qed "one_inverse";
 
 
-goal thy "ALL x. EX! y. y * x = (1::'a::group)";
+Goal "ALL x. EX! y. y * x = (1::'a::group)";
 by (rtac allI 1);
 by (rtac ex1I 1);
 by (rtac left_inverse 1);
@@ -108,7 +108,7 @@
 qed "ex1_inverse";
 
 
-goal thy "inverse (x * y) = inverse y * inverse (x::'a::group)";
+Goal "inverse (x * y) = inverse y * inverse (x::'a::group)";
 by (rtac sym 1);
 by (rtac mp 1);
 by (rtac one_inverse 1);
@@ -122,7 +122,7 @@
 qed "inverse_times";
 
 
-goal thy "inverse (inverse x) = (x::'a::group)";
+Goal "inverse (inverse x) = (x::'a::group)";
 by (rtac sym 1);
 by (rtac (one_inverse RS mp) 1);
 by (rtac (ssub right_inverse) 1);
isabelle