# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264500788 -3600
# Node ID 60dd70913b440eaf1fe61fc96f70f413b4cb84bc
# Parent  da5e4b8317c77985fe5929a6c0e5cca9e1c4c1b8
tuned

diff -r da5e4b8317c7 -r 60dd70913b44 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Tue Jan 26 10:53:44 2010 +0100
+++ b/Quot/QuotList.thy	Tue Jan 26 11:13:08 2010 +0100
@@ -1,7 +1,12 @@
- theory QuotList
+(*  Title:      QuotList.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+*) 
+theory QuotList
 imports QuotMain List
 begin
 
+section {* Quotient infrastructure for the list type. *}
+
 fun
   list_rel
 where
@@ -12,9 +17,6 @@
 
 declare [[map list = (map, list_rel)]]
 
-
-
-text {* should probably be in Sum_Type.thy *}
 lemma split_list_all: 
   shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
   apply(auto)
diff -r da5e4b8317c7 -r 60dd70913b44 Quot/QuotOption.thy
--- a/Quot/QuotOption.thy	Tue Jan 26 10:53:44 2010 +0100
+++ b/Quot/QuotOption.thy	Tue Jan 26 11:13:08 2010 +0100
@@ -5,7 +5,7 @@
 imports QuotMain
 begin
 
-section {* Quotient infrastructure for option type *}
+section {* Quotient infrastructure for the option type. *}
 
 fun
   option_rel
@@ -20,10 +20,10 @@
 text {* should probably be in Option.thy *}
 lemma split_option_all: 
   shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
-apply(auto)
-apply(case_tac x)
-apply(simp_all)
-done
+  apply(auto)
+  apply(case_tac x)
+  apply(simp_all)
+  done
 
 lemma option_quotient[quot_thm]:
   assumes q: "Quotient R Abs Rep"
diff -r da5e4b8317c7 -r 60dd70913b44 Quot/QuotProd.thy
--- a/Quot/QuotProd.thy	Tue Jan 26 10:53:44 2010 +0100
+++ b/Quot/QuotProd.thy	Tue Jan 26 11:13:08 2010 +0100
@@ -5,7 +5,7 @@
 imports QuotMain
 begin
 
-section {* Quotient infrastructure for product type *}
+section {* Quotient infrastructure for the product type. *}
 
 fun
   prod_rel
@@ -44,7 +44,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
-by simp
+  by simp
 
 lemma Pair_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
diff -r da5e4b8317c7 -r 60dd70913b44 Quot/QuotSum.thy
--- a/Quot/QuotSum.thy	Tue Jan 26 10:53:44 2010 +0100
+++ b/Quot/QuotSum.thy	Tue Jan 26 11:13:08 2010 +0100
@@ -5,6 +5,8 @@
 imports QuotMain
 begin
 
+section {* Quotient infrastructure for the sum type. *}
+
 fun
   sum_rel
 where
@@ -25,10 +27,10 @@
 text {* should probably be in Sum_Type.thy *}
 lemma split_sum_all: 
   shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
-apply(auto)
-apply(case_tac x)
-apply(simp_all)
-done
+  apply(auto)
+  apply(case_tac x)
+  apply(simp_all)
+  done
 
 lemma sum_equivp[quot_equiv]:
   assumes a: "equivp R1"