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

author | wenzelm |

Tue, 27 Aug 2002 11:06:20 +0200 | |

changeset 13530 | 4813fdc0ef17 |

parent 13529 | 49a0ad8f175e |

child 13531 | 5825aef91ac5 |

Thm.proof_of;

src/Pure/Proof/proof_syntax.ML | file | annotate | diff | comparison | revisions | |

src/Pure/Thy/thm_deps.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/Proof/proof_syntax.ML Tue Aug 27 11:06:07 2002 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Tue Aug 27 11:06:20 2002 +0200 @@ -147,7 +147,7 @@ | "thm" :: xs => let val name = NameSpace.pack xs; in (case assoc (thms, name) of - Some thm => fst (strip_combt (#2 (#der (rep_thm thm)))) + Some thm => fst (strip_combt (Thm.proof_of thm)) | None => (case Symtab.lookup (tab, name) of Some prf => prf | None => error ("Unknown theorem " ^ quote name)))

--- a/src/Pure/Thy/thm_deps.ML Tue Aug 27 11:06:07 2002 +0200 +++ b/src/Pure/Thy/thm_deps.ML Tue Aug 27 11:06:20 2002 +0200 @@ -70,7 +70,7 @@ let val _ = writeln "Generating graph ..."; val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), - map (#2 o #der o Thm.rep_thm) thms)))); + map Thm.proof_of thms)))); val path = File.tmp_path (Path.unpack "theorems.graph"); val _ = Present.write_graph gra path; val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");