src/HOL/Nonstandard_Analysis/transfer_principle.ML
changeset 67636 e4eb21f8331c
parent 67635 28f926146986
child 69597 ff784d5a5bfb
equal deleted inserted replaced
67635:28f926146986 67636:e4eb21f8331c
   106 fun map_refolds f = Data.map
   106 fun map_refolds f = Data.map
   107   (fn {intros,unfolds,refolds,consts} =>
   107   (fn {intros,unfolds,refolds,consts} =>
   108     {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
   108     {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
   109 in
   109 in
   110 
   110 
   111 val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm);
   111 val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm o Thm.trim_context);
   112 val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
   112 val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
   113 
   113 
   114 val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm);
   114 val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm o Thm.trim_context);
   115 val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm);
   115 val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm);
   116 
   116 
   117 val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm);
   117 val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm o Thm.trim_context);
   118 val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
   118 val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
   119 
   119 
   120 end
   120 end
   121 
   121 
   122 fun add_const c = Context.theory_map (Data.map
   122 fun add_const c = Context.theory_map (Data.map