equal
deleted
inserted
replaced
70 |
70 |
71 |
71 |
72 (* retrieve theorems *) |
72 (* retrieve theorems *) |
73 |
73 |
74 fun get_thms thy xname = |
74 fun get_thms thy xname = |
75 #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none)); |
75 #thms (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none)); |
76 |
76 |
77 fun get_thm thy xname = |
77 fun get_thm thy xname = |
78 Facts.the_single (xname, Position.none) (get_thms thy xname); |
78 Facts.the_single (xname, Position.none) (get_thms thy xname); |
79 |
79 |
80 fun all_thms_of thy verbose = |
80 fun all_thms_of thy verbose = |