338 | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = |
338 | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = |
339 add_hol4_const_mapping thyname constname true fullcname thy |
339 add_hol4_const_mapping thyname constname true fullcname thy |
340 | delta (Hol_move (fullname, moved_thmname)) thy = |
340 | delta (Hol_move (fullname, moved_thmname)) thy = |
341 add_hol4_move fullname moved_thmname thy |
341 add_hol4_move fullname moved_thmname thy |
342 | delta (Defs (thmname, eq)) thy = |
342 | delta (Defs (thmname, eq)) thy = |
343 snd (PureThy.add_defs false [((thmname, eq), [])] thy) |
343 snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy) |
344 | delta (Hol_theorem (thyname, thmname, th)) thy = |
344 | delta (Hol_theorem (thyname, thmname, th)) thy = |
345 add_hol4_theorem thyname thmname ([], th_of thy th) thy |
345 add_hol4_theorem thyname thmname ([], th_of thy th) thy |
346 | delta (Typedef (thmname, typ, c, repabs, th)) thy = |
346 | delta (Typedef (thmname, typ, c, repabs, th)) thy = |
347 snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy) |
347 snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy) |
348 | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy = |
348 | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy = |