src/Provers/classical.ML
changeset 45375 7fe19930dfc9
parent 42817 7e819eb7dabb
child 46459 73823dbbecc4
equal deleted inserted replaced
45374:e99fd663c4a3 45375:7fe19930dfc9
   846 val safe_intro = attrib o addSI;
   846 val safe_intro = attrib o addSI;
   847 val safe_dest = attrib o addSD;
   847 val safe_dest = attrib o addSD;
   848 val haz_elim = attrib o addE;
   848 val haz_elim = attrib o addE;
   849 val haz_intro = attrib o addI;
   849 val haz_intro = attrib o addI;
   850 val haz_dest = attrib o addD;
   850 val haz_dest = attrib o addD;
   851 val rule_del = attrib delrule o Context_Rules.rule_del;
   851 
       
   852 val rule_del =
       
   853   Thm.declaration_attribute (fn th => fn context =>
       
   854     context |> map_cs (delrule (SOME context) th) |>
       
   855     Thm.attribute_declaration Context_Rules.rule_del th);
   852 
   856 
   853 
   857 
   854 
   858 
   855 (** concrete syntax of attributes **)
   859 (** concrete syntax of attributes **)
   856 
   860