332 fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th)) |
332 fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th)) |
333 | delta (Hol_mapping (thyname, thmname, isaname)) thy = |
333 | delta (Hol_mapping (thyname, thmname, isaname)) thy = |
334 add_hol4_mapping thyname thmname isaname thy |
334 add_hol4_mapping thyname thmname isaname thy |
335 | delta (Hol_pending (thyname, thmname, th)) thy = |
335 | delta (Hol_pending (thyname, thmname, th)) thy = |
336 add_hol4_pending thyname thmname ([], th_of thy th) thy |
336 add_hol4_pending thyname thmname ([], th_of thy th) thy |
337 | delta (Consts cs) thy = Sign.add_consts_i cs thy |
337 | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy |
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 [((Binding.name 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, (t, vs, mx), 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 (Option.map Binding.name thmname) (Binding.name t, vs, mx) c |
|
348 (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy) |
348 | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy = |
349 | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy = |
349 add_hol4_type_mapping thyname tycname true fulltyname thy |
350 add_hol4_type_mapping thyname tycname true fulltyname thy |
350 | delta (Indexed_theorem (i, th)) thy = |
351 | delta (Indexed_theorem (i, th)) thy = |
351 (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy) |
352 (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy) |
352 | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy) |
353 | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy) |