src/Tools/atomize_elim.ML
changeset 31902 862ae16a799d
parent 30515 bca05b17b618
child 33002 f3f02f36a3e2
equal deleted inserted replaced
31901:e280491f36b8 31902:862ae16a799d
    18 
    18 
    19 structure AtomizeElim : ATOMIZE_ELIM =
    19 structure AtomizeElim : ATOMIZE_ELIM =
    20 struct
    20 struct
    21 
    21 
    22 (* theory data *)
    22 (* theory data *)
    23 structure AtomizeElimData = NamedThmsFun(
    23 
       
    24 structure AtomizeElimData = Named_Thms
       
    25 (
    24   val name = "atomize_elim";
    26   val name = "atomize_elim";
    25   val description = "atomize_elim rewrite rule";
    27   val description = "atomize_elim rewrite rule";
    26 );
    28 );
    27 
    29 
    28 val declare_atomize_elim = AtomizeElimData.add
    30 val declare_atomize_elim = AtomizeElimData.add