1signature TheoryReader = 2sig 3 4 exception TheoryReader of string 5 val load_thydata : string -> string -> (string, Thm.thm) Redblackmap.dict 6 7end 8 9(* [load_thydata thyname fname] loads the filename and makes the appropriate 10 changes to the theory hierarchy in response to the data stored there. In 11 other words, this is done mostly for the side-effects. The map returned 12 allows <nm>Theory.sml files to then bind SML identifiers corresponding to 13 theorem names to theorem values. 14*) 15