src/HOL/Hyperreal/transfer.ML
changeset 17332 4910cf8c0cd2
parent 17329 72637e062a0d
child 17333 605c97701833
     1.1 --- a/src/HOL/Hyperreal/transfer.ML	Mon Sep 12 23:13:46 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/transfer.ML	Mon Sep 12 23:14:41 2005 +0200
     1.3 @@ -127,13 +127,16 @@
     1.4  val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac;
     1.5  
     1.6  val setup =
     1.7 -  [ TransferData.init
     1.8 -  , Attrib.add_attributes
     1.9 -    [ ("transfer_intro", intro_attr, "transfer introduction rule")
    1.10 -    , ("transfer_unfold", unfold_attr, "transfer unfolding rule")
    1.11 -    , ("transfer_refold", refold_attr, "transfer refolding rule")
    1.12 -    ]
    1.13 -  , Method.add_method
    1.14 +  [ TransferData.init,
    1.15 +    Attrib.add_attributes
    1.16 +    [ ("transfer_intro", intro_attr,
    1.17 +       "declaration of transfer introduction rule"),
    1.18 +      ("transfer_unfold", unfold_attr,
    1.19 +       "declaration of transfer unfolding rule"),
    1.20 +      ("transfer_refold", refold_attr,
    1.21 +       "declaration of transfer refolding rule")
    1.22 +    ],
    1.23 +    Method.add_method
    1.24      ("transfer", Method.thms_args transfer_method, "transfer principle")
    1.25    ];
    1.26