src/HOL/Hyperreal/transfer.ML
changeset 18708 4b3dadb4fe33
parent 17985 d5d576b72371
child 18729 216e31270509
     1.1 --- a/src/HOL/Hyperreal/transfer.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Hyperreal/transfer.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val transfer_tac: thm list -> int -> tactic
     1.6    val add_const: string -> theory -> theory
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  structure Transfer: TRANSFER_TAC =
    1.12 @@ -127,17 +127,15 @@
    1.13  val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac;
    1.14  
    1.15  val setup =
    1.16 -  [ TransferData.init,
    1.17 -    Attrib.add_attributes
    1.18 -    [ ("transfer_intro", intro_attr,
    1.19 -       "declaration of transfer introduction rule"),
    1.20 -      ("transfer_unfold", unfold_attr,
    1.21 -       "declaration of transfer unfolding rule"),
    1.22 -      ("transfer_refold", refold_attr,
    1.23 -       "declaration of transfer refolding rule")
    1.24 -    ],
    1.25 -    Method.add_method
    1.26 -    ("transfer", Method.thms_args transfer_method, "transfer principle")
    1.27 -  ];
    1.28 +  TransferData.init #>
    1.29 +  Attrib.add_attributes
    1.30 +    [("transfer_intro", intro_attr,
    1.31 +      "declaration of transfer introduction rule"),
    1.32 +     ("transfer_unfold", unfold_attr,
    1.33 +      "declaration of transfer unfolding rule"),
    1.34 +     ("transfer_refold", refold_attr,
    1.35 +      "declaration of transfer refolding rule")] #>
    1.36 +  Method.add_method
    1.37 +    ("transfer", Method.thms_args transfer_method, "transfer principle");
    1.38  
    1.39  end;