src/HOL/Nat_Transfer.thy
changeset 35551 85aada96578b
parent 33340 a165b97f3658
child 35644 d20cf282342e
     1.1 --- a/src/HOL/Nat_Transfer.thy	Wed Mar 03 17:21:45 2010 +0100
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Wed Mar 03 17:21:47 2010 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
     1.5    by (simp add: TransferMorphism_def)
     1.6  
     1.7 -declare TransferMorphism_nat_int[transfer
     1.8 +declare TransferMorphism_nat_int [transfer
     1.9    add mode: manual
    1.10    return: nat_0_le
    1.11    labels: natint
    1.12 @@ -80,7 +80,7 @@
    1.13        (nat (x::int) dvd nat y) = (x dvd y)"
    1.14    by (auto simp add: zdvd_int)
    1.15  
    1.16 -declare TransferMorphism_nat_int[transfer add return:
    1.17 +declare TransferMorphism_nat_int [transfer add return:
    1.18    transfer_nat_int_numerals
    1.19    transfer_nat_int_functions
    1.20    transfer_nat_int_function_closures
    1.21 @@ -118,7 +118,7 @@
    1.22      (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
    1.23    by auto
    1.24  
    1.25 -declare TransferMorphism_nat_int[transfer add
    1.26 +declare TransferMorphism_nat_int [transfer add
    1.27    return: transfer_nat_int_quantifiers
    1.28    cong: all_cong ex_cong]
    1.29  
    1.30 @@ -190,7 +190,7 @@
    1.31      {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
    1.32    by auto
    1.33  
    1.34 -declare TransferMorphism_nat_int[transfer add
    1.35 +declare TransferMorphism_nat_int [transfer add
    1.36    return: transfer_nat_int_set_functions
    1.37      transfer_nat_int_set_function_closures
    1.38      transfer_nat_int_set_relations
    1.39 @@ -262,7 +262,7 @@
    1.40    apply (subst setprod_cong, assumption, auto)
    1.41  done
    1.42  
    1.43 -declare TransferMorphism_nat_int[transfer add
    1.44 +declare TransferMorphism_nat_int [transfer add
    1.45    return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
    1.46      transfer_nat_int_sum_prod_closure
    1.47    cong: transfer_nat_int_sum_prod_cong]
    1.48 @@ -275,7 +275,7 @@
    1.49  lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
    1.50    by (simp add: TransferMorphism_def)
    1.51  
    1.52 -declare TransferMorphism_int_nat[transfer add
    1.53 +declare TransferMorphism_int_nat [transfer add
    1.54    mode: manual
    1.55  (*  labels: int-nat *)
    1.56    return: nat_int
    1.57 @@ -326,7 +326,7 @@
    1.58      "(int x dvd int y) = (x dvd y)"
    1.59    by (auto simp add: zdvd_int)
    1.60  
    1.61 -declare TransferMorphism_int_nat[transfer add return:
    1.62 +declare TransferMorphism_int_nat [transfer add return:
    1.63    transfer_int_nat_numerals
    1.64    transfer_int_nat_functions
    1.65    transfer_int_nat_function_closures
    1.66 @@ -346,7 +346,7 @@
    1.67    apply auto
    1.68  done
    1.69  
    1.70 -declare TransferMorphism_int_nat[transfer add
    1.71 +declare TransferMorphism_int_nat [transfer add
    1.72    return: transfer_int_nat_quantifiers]
    1.73  
    1.74  
    1.75 @@ -401,7 +401,7 @@
    1.76      {(x::nat). P x} = {x. P' x}"
    1.77    by auto
    1.78  
    1.79 -declare TransferMorphism_int_nat[transfer add
    1.80 +declare TransferMorphism_int_nat [transfer add
    1.81    return: transfer_int_nat_set_functions
    1.82      transfer_int_nat_set_function_closures
    1.83      transfer_int_nat_set_relations
    1.84 @@ -433,7 +433,7 @@
    1.85    apply (subst int_setprod, auto simp add: cong: setprod_cong)
    1.86  done
    1.87  
    1.88 -declare TransferMorphism_int_nat[transfer add
    1.89 +declare TransferMorphism_int_nat [transfer add
    1.90    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
    1.91    cong: setsum_cong setprod_cong]
    1.92