tuned white space;
authorwenzelm
Mon Oct 26 20:02:37 2009 +0100 (2009-10-26)
changeset 33209d36ca3960e33
parent 33208 1e064a1b3006
child 33210 94ae82a4452f
tuned white space;
src/HOL/Induct/LList.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Rational.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Induct/LList.thy	Mon Oct 26 15:36:50 2009 +0100
     1.2 +++ b/src/HOL/Induct/LList.thy	Mon Oct 26 20:02:37 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Induct/LList.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7  
     1.8  Shares NIL, CONS, List_case with List.thy
     1.9 @@ -906,8 +905,8 @@
    1.10  by (rule_tac l = l1 in llist_fun_equalityI, auto)
    1.11  
    1.12  setup {*
    1.13 -Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
    1.14 -                            (map dest_Const [@{term LNil}, @{term LCons}])
    1.15 +  Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
    1.16 +    (map dest_Const [@{term LNil}, @{term LCons}])
    1.17  *}
    1.18  
    1.19  end
     2.1 --- a/src/HOL/Library/Coinductive_List.thy	Mon Oct 26 15:36:50 2009 +0100
     2.2 +++ b/src/HOL/Library/Coinductive_List.thy	Mon Oct 26 20:02:37 2009 +0100
     2.3 @@ -850,8 +850,8 @@
     2.4  qed
     2.5  
     2.6  setup {*
     2.7 -Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
     2.8 -                            (map dest_Const [@{term LNil}, @{term LCons}])
     2.9 +  Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
    2.10 +    (map dest_Const [@{term LNil}, @{term LCons}])
    2.11  *}
    2.12  
    2.13  end
     3.1 --- a/src/HOL/Rational.thy	Mon Oct 26 15:36:50 2009 +0100
     3.2 +++ b/src/HOL/Rational.thy	Mon Oct 26 20:02:37 2009 +0100
     3.3 @@ -1064,22 +1064,22 @@
     3.4  *}
     3.5  
     3.6  setup {*
     3.7 -Nitpick.register_frac_type @{type_name rat}
     3.8 -    [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
     3.9 -     (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
    3.10 -     (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
    3.11 -     (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
    3.12 -     (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
    3.13 -     (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
    3.14 -     (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
    3.15 -     (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
    3.16 -     (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
    3.17 -     (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
    3.18 +  Nitpick.register_frac_type @{type_name rat}
    3.19 +   [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
    3.20 +    (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
    3.21 +    (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
    3.22 +    (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
    3.23 +    (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
    3.24 +    (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
    3.25 +    (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
    3.26 +    (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
    3.27 +    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
    3.28 +    (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
    3.29  *}
    3.30  
    3.31  lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
    3.32 -    number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
    3.33 -    plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
    3.34 -    zero_rat_inst.zero_rat
    3.35 +  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
    3.36 +  plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
    3.37 +  zero_rat_inst.zero_rat
    3.38  
    3.39  end
     4.1 --- a/src/HOL/RealDef.thy	Mon Oct 26 15:36:50 2009 +0100
     4.2 +++ b/src/HOL/RealDef.thy	Mon Oct 26 20:02:37 2009 +0100
     4.3 @@ -1186,15 +1186,15 @@
     4.4  *}
     4.5  
     4.6  setup {*
     4.7 -Nitpick.register_frac_type @{type_name real}
     4.8 -    [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
     4.9 -     (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
    4.10 -     (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
    4.11 -     (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
    4.12 -     (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
    4.13 -     (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
    4.14 -     (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
    4.15 -     (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
    4.16 +  Nitpick.register_frac_type @{type_name real}
    4.17 +   [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
    4.18 +    (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
    4.19 +    (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
    4.20 +    (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
    4.21 +    (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
    4.22 +    (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
    4.23 +    (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
    4.24 +    (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
    4.25  *}
    4.26  
    4.27  lemmas [nitpick_def] = inverse_real_inst.inverse_real