src/HOL/Import/hol4rews.ML
changeset 18708 4b3dadb4fe33
parent 18358 0a733e11021a
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Import/hol4rews.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -758,24 +758,25 @@
     1.4  	    |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
     1.5  in
     1.6  val hol4_setup =
     1.7 -    [HOL4Rewrites.init,
     1.8 -     HOL4Maps.init,
     1.9 -     HOL4UNames.init,
    1.10 -     HOL4DefMaps.init,
    1.11 -     HOL4Moves.init,
    1.12 -     HOL4CMoves.init,
    1.13 -     HOL4ConstMaps.init,
    1.14 -     HOL4Rename.init,
    1.15 -     HOL4TypeMaps.init,
    1.16 -     HOL4Pending.init,
    1.17 -     HOL4Thms.init,
    1.18 -     HOL4Dump.init,
    1.19 -     HOL4DefThy.init,
    1.20 -     HOL4Imports.init,
    1.21 -     ImportSegment.init,
    1.22 -     initial_maps,
    1.23 -     Attrib.add_attributes [("hol4rew",
    1.24 -			     (Attrib.no_args add_hol4_rewrite,
    1.25 -			      Attrib.no_args Attrib.undef_local_attribute),
    1.26 -			     "HOL4 rewrite rule")]]
    1.27 +  HOL4Rewrites.init #>
    1.28 +  HOL4Maps.init #>
    1.29 +  HOL4UNames.init #>
    1.30 +  HOL4DefMaps.init #>
    1.31 +  HOL4Moves.init #>
    1.32 +  HOL4CMoves.init #>
    1.33 +  HOL4ConstMaps.init #>
    1.34 +  HOL4Rename.init #>
    1.35 +  HOL4TypeMaps.init #>
    1.36 +  HOL4Pending.init #>
    1.37 +  HOL4Thms.init #>
    1.38 +  HOL4Dump.init #>
    1.39 +  HOL4DefThy.init #>
    1.40 +  HOL4Imports.init #>
    1.41 +  ImportSegment.init #>
    1.42 +  initial_maps #>
    1.43 +  Attrib.add_attributes
    1.44 +    [("hol4rew",
    1.45 +      (Attrib.no_args add_hol4_rewrite,
    1.46 +       Attrib.no_args Attrib.undef_local_attribute),
    1.47 +      "HOL4 rewrite rule")]
    1.48  end