# HG changeset patch
# User wenzelm
# Date 1256583757 -3600
# Node ID d36ca3960e330571ad72f142bf043093ca501f5b
# Parent  1e064a1b3006c55ac7bb84ddd2cd06ba3deb6148
tuned white space;

diff -r 1e064a1b3006 -r d36ca3960e33 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Mon Oct 26 15:36:50 2009 +0100
+++ b/src/HOL/Induct/LList.thy	Mon Oct 26 20:02:37 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Induct/LList.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Shares NIL, CONS, List_case with List.thy
@@ -906,8 +905,8 @@
 by (rule_tac l = l1 in llist_fun_equalityI, auto)
 
 setup {*
-Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
-                            (map dest_Const [@{term LNil}, @{term LCons}])
+  Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
+    (map dest_Const [@{term LNil}, @{term LCons}])
 *}
 
 end
diff -r 1e064a1b3006 -r d36ca3960e33 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Mon Oct 26 15:36:50 2009 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Mon Oct 26 20:02:37 2009 +0100
@@ -850,8 +850,8 @@
 qed
 
 setup {*
-Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
-                            (map dest_Const [@{term LNil}, @{term LCons}])
+  Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
+    (map dest_Const [@{term LNil}, @{term LCons}])
 *}
 
 end
diff -r 1e064a1b3006 -r d36ca3960e33 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Mon Oct 26 15:36:50 2009 +0100
+++ b/src/HOL/Rational.thy	Mon Oct 26 20:02:37 2009 +0100
@@ -1064,22 +1064,22 @@
 *}
 
 setup {*
-Nitpick.register_frac_type @{type_name rat}
-    [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
-     (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
-     (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
-     (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
-     (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
-     (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
-     (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
-     (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
-     (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
-     (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
+  Nitpick.register_frac_type @{type_name rat}
+   [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
+    (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
+    (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
+    (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
+    (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
+    (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
+    (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
+    (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
+    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
+    (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
 *}
 
 lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
-    number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
-    plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
-    zero_rat_inst.zero_rat
+  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
+  plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
+  zero_rat_inst.zero_rat
 
 end
diff -r 1e064a1b3006 -r d36ca3960e33 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Mon Oct 26 15:36:50 2009 +0100
+++ b/src/HOL/RealDef.thy	Mon Oct 26 20:02:37 2009 +0100
@@ -1186,15 +1186,15 @@
 *}
 
 setup {*
-Nitpick.register_frac_type @{type_name real}
-    [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
-     (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
-     (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
-     (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
-     (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
-     (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
-     (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
-     (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
+  Nitpick.register_frac_type @{type_name real}
+   [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
+    (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
+    (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
+    (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
+    (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
+    (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
+    (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
+    (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
 *}
 
 lemmas [nitpick_def] = inverse_real_inst.inverse_real