diff --git a/fol/Groups.v b/fol/Groups.v
index 8efeb60e31e1f05dc5f164c562608131b9babb2c..28857785113579db58599da08751f923fe33737c 100644
--- a/fol/Groups.v
+++ b/fol/Groups.v
@@ -1,12 +1,22 @@
 
 (** Ziel dieses Files ist es, All- und Existenzquantoren in Kombination mit Gleichheits-Einführung und Eliminierung anhand von Gruppentheorie zu üben. *)
 
-  (** Wir benutzen hier ein paar bereits in der Standardbibliothek implementierte Funktionen: *)
+(** Wir benutzen hier ein paar bereits in der Standardbibliothek implementierte Funktionen: *)
 
-Print bool.
 Print xorb.
+(**
+<<
+fun b1 b2 : bool => if b1 then if b2 then false else true else b2
+     : bool -> bool -> bool
+>>
+ *)
 
-(** Wir möchten nun zeigen, dass die Menge bool, bestehend aus true und false, zusammen mit der Operation xorb eine Gruppe bildet. Dazu müssen wir sowohl Assoziativität als auch die Existenz eines neutralen Elements zeigen. Außerdem brauchen wir noch eine Inversenfunktion. *)
+(** Wir möchten nun zeigen, dass die Menge [bool], bestehend aus 
+    [true] und [false], zusammen mit der Operation [xorb] eine Gruppe 
+    bildet. Dazu müssen wir sowohl Assoziativität als auch die Existenz 
+    eines neutralen Elements zeigen. Außerdem brauchen wir noch eine 
+    Inversenfunktion. 
+*)
 
 Definition is_assoc (G : Set) (f : G -> G -> G) : Prop := forall x y z, f (f x y) z = f x (f y z).
 
@@ -14,7 +24,10 @@ Definition is_left_id (G : Set) (f : G -> G -> G) (e : G) : Prop := forall (x :
 
 Definition is_left_inv (G : Set) (f : G -> G -> G) (e : G) (i : G -> G) : Prop := forall (x : G), f (i x) x = e.
 
-(** Bevor wir mit dem Beweis starten, bringen wir bool noch in unseren (prädikatenlogischen) Kontext: *)
+(** Bevor wir mit dem Beweis starten, 
+    bringen wir bool noch in unseren 
+    (prädikatenlogischen) Kontext: 
+*)
 
 Lemma bool_charac : forall (x : bool), x = true \/ x = false.
 Proof.
@@ -26,7 +39,10 @@ Proof.
   destruct x. (** Was ist hier passiert? *)
 Admitted.
 
-(** Hier noch ein Tipp zum "Mindsetting" in dieser Aufgabe: Man sollte hier differenzieren zwischen der Menge an Termen "bool", die aus den beiden Termen "true" und "false" besteht, und First-Order-Logic, in Coq durch "Prop" dargestellt. *)
+(** Hier noch ein Tipp zum "Mindsetting" in dieser Aufgabe: 
+    Man sollte hier differenzieren zwischen der Menge an Termen 
+    "[bool]", die aus den beiden Termen "[true]" und "[false]" besteht, und First-Order-Logic, in Coq durch "[Prop]" dargestellt. *)
+
 Theorem xor_assoc : is_assoc bool xorb.
 Proof.
   unfold is_assoc.
@@ -46,8 +62,7 @@ Proof.
     }
   destruct H1 as [A1|A1].
   rewrite A1.
-  Print xorb.
-  simpl. (** simpl sorgt hier dafür, dass die Funktion xorb teilweise ausgewertet wird. Das ist möglich, da das erste Argument bekannt ist. Vgl. mit der Definition von xorb. *)
+  simpl. (** [simpl] sorgt hier dafür, dass die Funktion [xorb] teilweise ausgewertet wird. Das ist möglich, da das erste Argument bekannt ist. Vgl. mit der Definition von [xorb]. *)
 
   Restart.
 
@@ -57,8 +72,12 @@ Admitted.
 
 (** Hier gibt es jetzt zwei kreative Stellen:
    1) Finde das neutrale Element.
-   2) Finde die Inversen-Funktion. Tipp: Angenommen, x ist das Inverse zu sich selbst (also zu x), dann kann man das als Funktion (fun x => x) angeben.
+   2) Finde die Inversen-Funktion. 
+
+   Tipp: Angenommen, [x] ist das Inverse zu sich selbst (also zu [x]), 
+   dann kann man das als Funktion ([fun x => x]) angeben.
  *)
+
 Theorem xor_left_id_inv_exists : exists (e : bool), is_left_id bool xorb e /\ exists (i : bool -> bool), is_left_inv bool xorb e i.
 Proof.
   unfold is_left_id, is_left_inv.