summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 21 Mar 1996 11:09:47 +0100 | |

changeset 1598 | 6f4d995590fd |

parent 1597 | 54ece585bf62 |

child 1599 | b11ac7072422 |

For the new version of name_thm. Now the same theorem
is stored as is returned, as both contain a label and a link to the
previous derivation. So get_thm no longer needs to attach a label to
its resulting theorem.

--- a/src/Pure/Thy/thy_read.ML Thu Mar 21 11:06:59 1996 +0100 +++ b/src/Pure/Thy/thy_read.ML Thu Mar 21 11:09:47 1996 +0100 @@ -1073,8 +1073,8 @@ | None => () end; - (*Return version with trivial proof object; store original version *) - val thm' = Thm.name_thm (the theory, name, thm) handle OPTION _ => thm + (*Label this theorem*) + val thm' = Thm.name_thm (name, thm) in loaded_thys := Symtab.update ((thy_name, ThyInfo {path = path, children = children, parents = parents, @@ -1118,8 +1118,7 @@ let val ThyInfo {thms, ...} = the (get_thyinfo name); in thms end; -(*Get a stored theorem specified by theory and name. - Derivation has the form Theorem(thy,name). *) +(*Get a stored theorem specified by theory and name. *) fun get_thm thy name = let fun get [] [] searched = raise THEORY ("get_thm: no theorem " ^ quote name, [thy]) @@ -1127,7 +1126,7 @@ get (ng \\ searched) [] searched | get (t::ts) ng searched = (case Symtab.lookup (thmtab_of_name t, name) of - Some thm => Thm.name_thm(thy,name,thm) + Some thm => thm | None => get ts (ng union (parents_of_name t)) (t::searched)); val (tname, _) = thyinfo_of_sign (sign_of thy); @@ -1303,7 +1302,7 @@ Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms)) end; -fun print_theory thy = (Drule.print_theory thy; print_thms thy); +fun print_theory thy = (Display.print_theory thy; print_thms thy); (*** Misc functions ***)