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

author | wenzelm |

Fri, 03 Sep 1999 13:55:46 +0200 | |

changeset 7446 | f43d3670a3cd |

parent 7445 | 6dd6110968c9 |

child 7447 | d09f39cd3b6e |

added no_qed;

doc-src/Ref/goals.tex | file | annotate | diff | comparison | revisions | |

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

--- a/doc-src/Ref/goals.tex Fri Sep 03 10:14:28 1999 +0200 +++ b/doc-src/Ref/goals.tex Fri Sep 03 13:55:46 1999 +0200 @@ -135,6 +135,7 @@ \index{theorems!extracting proved} \begin{ttbox} qed : string -> unit +no_qed : unit -> unit result : unit -> thm uresult : unit -> thm bind_thm : string * thm -> unit @@ -147,6 +148,11 @@ It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem using \texttt{result()} and stores it the theorem database associated with its theory. See below for details. + +\item[\ttindexbold{no_qed}();] indicates that the proof is not concluded by a + proper \texttt{qed} command. This is a do-nothing operation, it merely + helps user interfaces such as Proof~General \cite{proofgeneral} to figure + out the structure of the {\ML} text. \item[\ttindexbold{result}()]\index{assumptions!of main goal} returns the final theorem, after converting the free variables to

--- a/src/Pure/Thy/thm_database.ML Fri Sep 03 10:14:28 1999 +0200 +++ b/src/Pure/Thy/thm_database.ML Fri Sep 03 13:55:46 1999 +0200 @@ -14,6 +14,7 @@ val qed: string -> unit val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit + val no_qed: unit -> unit (*these peek at the proof state!*) val thms_containing: xstring list -> (string * thm) list val findI: int -> (string * thm) list @@ -79,10 +80,13 @@ fun bind_thm (name, thm) = ml_store_thm (name, standard thm); fun bind_thms (name, thms) = ml_store_thms (name, map standard thms); + fun qed name = ml_store_thm (name, Goals.result ()); fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf); fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf); +fun no_qed () = (); + (** retrieve theorems **)