src/Tools/atomize_elim.ML
changeset 30515 bca05b17b618
parent 30510 4120fc59dd85
child 31902 862ae16a799d
equal deleted inserted replaced
30514:9455ecc7796d 30515:bca05b17b618
   129     in
   129     in
   130       quantify_thesis
   130       quantify_thesis
   131       THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
   131       THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
   132     end)
   132     end)
   133 
   133 
   134 val setup = Method.add_methods
   134 val setup =
   135   [("atomize_elim", Method.ctxt_args (SIMPLE_METHOD' o atomize_elim_tac),
   135   Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
   136     "convert obtains statement to atomic object logic goal")]
   136     "convert obtains statement to atomic object logic goal"
   137   #> AtomizeElimData.setup
   137   #> AtomizeElimData.setup
   138 
   138 
   139 end
   139 end