# HG changeset patch # User wenzelm # Date 1004562002 -3600 # Node ID 72fd225a5aa2d69944fa5409c4832cf4725a6a90 # Parent 29159339101018c35d4d199df487972dc6b8ba1c global statements: locale argument; diff -r 291593391010 -r 72fd225a5aa2 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Oct 31 21:59:25 2001 +0100 +++ b/src/Pure/Isar/isar_syn.ML Wed Oct 31 22:00:02 2001 +0100 @@ -284,35 +284,39 @@ (* statements *) -fun statement f = P.opt_thm_name ":" -- P.propp -- P.marg_comment >> f; +val locale = Scan.option (P.$$$ "(" |-- P.!!! (P.$$$ "in" |-- P.xname --| P.$$$ ")")); +val statement = P.opt_thm_name ":" -- P.propp -- P.marg_comment; val theoremP = OuterSyntax.command "theorem" "state theorem" K.thy_goal - (statement (IsarThy.theorem Drule.theoremK) >> (Toplevel.print oo Toplevel.theory_to_proof)); + (locale -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o + uncurry (IsarThy.theorem Drule.theoremK))); val lemmaP = OuterSyntax.command "lemma" "state lemma" K.thy_goal - (statement (IsarThy.theorem Drule.lemmaK) >> (Toplevel.print oo Toplevel.theory_to_proof)); + (locale -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o + uncurry (IsarThy.theorem Drule.lemmaK))); val corollaryP = OuterSyntax.command "corollary" "state corollary" K.thy_goal - (statement (IsarThy.theorem Drule.corollaryK) >> (Toplevel.print oo Toplevel.theory_to_proof)); + (locale -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o + uncurry (IsarThy.theorem Drule.corollaryK))); val showP = OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal - (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof' f)); + (statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.show)); val haveP = OuterSyntax.command "have" "state local goal" K.prf_goal - (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f)); + (statement >> ((Toplevel.print oo Toplevel.proof) o IsarThy.have)); val thusP = OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal - (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof' f)); + (statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.thus)); val henceP = OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal - (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f)); + (statement >> ((Toplevel.print oo Toplevel.proof) o IsarThy.hence)); (* facts *) diff -r 291593391010 -r 72fd225a5aa2 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Wed Oct 31 21:59:25 2001 +0100 +++ b/src/Pure/Isar/isar_thy.ML Wed Oct 31 22:00:02 2001 +0100 @@ -91,9 +91,11 @@ -> ProofHistory.T -> ProofHistory.T val invoke_case_i: (string * string option list * Proof.context attribute list) * Comment.text -> ProofHistory.T -> ProofHistory.T - val theorem: string -> ((bstring * Args.src list) * (string * (string list * string list))) + val theorem: string -> string option -> + ((bstring * Args.src list) * (string * (string list * string list))) * Comment.text -> bool -> theory -> ProofHistory.T - val theorem_i: string -> ((bstring * theory attribute list) * (term * (term list * term list))) + val theorem_i: string -> string option -> + ((bstring * theory attribute list) * (term * (term list * term list))) * Comment.text -> bool -> theory -> ProofHistory.T val assume: (((string * Args.src list) * (string * (string list * string list)) list) * Comment.text) list -> ProofHistory.T -> ProofHistory.T @@ -420,12 +422,12 @@ in -fun theorem k (((name, src), s), comment_ignore) int thy = +fun theorem k loc (((name, src), s), comment_ignore) int thy = ProofHistory.init (Toplevel.undo_limit int) - (Proof.theorem k name (map (Attrib.global_attribute thy) src) s thy); + (Proof.theorem k loc name (map (Attrib.global_attribute thy) src) s thy); -fun theorem_i k (((name, atts), t), comment_ignore) int thy = - ProofHistory.init (Toplevel.undo_limit int) (Proof.theorem_i k name atts t thy); +fun theorem_i k loc (((name, atts), t), comment_ignore) int thy = + ProofHistory.init (Toplevel.undo_limit int) (Proof.theorem_i k loc name atts t thy); val assume = multi_statement Proof.assume o map Comment.ignore; val assume_i = multi_statement_i Proof.assume_i o map Comment.ignore;