--- a/NEWS Tue Oct 06 15:14:28 2015 +0200
+++ b/NEWS Tue Oct 06 15:39:00 2015 +0200
@@ -19,6 +19,9 @@
Command-line tool "isabelle update_theorems" updates theory sources
accordingly.
+* Toplevel theorem statement 'proposition' is another alias for
+'theorem'.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/Isar_Ref/Proof.thy Tue Oct 06 15:14:28 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Tue Oct 06 15:39:00 2015 +0200
@@ -379,6 +379,7 @@
@{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
@{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
@{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+ @{command_def "proposition"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
@{command_def "schematic_goal"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
@{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
@{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
@@ -387,13 +388,10 @@
@{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
- From a theory context, proof mode is entered by an initial goal
- command such as @{command "lemma"}, @{command "theorem"}, or
- @{command "corollary"}. Within a proof, new claims may be
- introduced locally as well; four variants are available here to
- indicate whether forward chaining of facts should be performed
- initially (via @{command_ref "then"}), and whether the final result
- is meant to solve some pending goal.
+ From a theory context, proof mode is entered by an initial goal command
+ such as @{command "lemma"}. Within a proof context, new claims may be
+ introduced locally; there are variants to interact with the overall proof
+ structure specifically, such as @{command have} or @{command show}.
Goals may consist of multiple statements, resulting in a list of
facts eventually. A pending multi-goal is internally represented as
@@ -421,7 +419,7 @@
@{rail \<open>
(@@{command lemma} | @@{command theorem} | @@{command corollary} |
- @@{command schematic_goal}) (stmt | statement)
+ @@{command proposition} | @@{command schematic_goal}) (stmt | statement)
;
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
stmt cond_stmt @{syntax for_fixes}
@@ -454,11 +452,9 @@
well, see also @{syntax "includes"} in \secref{sec:bundle} and
@{syntax context_elem} in \secref{sec:locale}.
- \item @{command "theorem"}~@{text "a: \<phi>"} and @{command
- "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command
- "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
- being of a different kind. This discrimination acts like a formal
- comment.
+ \item @{command "theorem"}, @{command "corollary"}, and @{command
+ "proposition"} are the same as @{command "lemma"}. The different command
+ names merely serve as a formal comment in the theory source.
\item @{command "schematic_goal"} is similar to @{command "theorem"},
but allows the statement to contain unbound schematic variables.
--- a/src/Pure/Isar/isar_syn.ML Tue Oct 06 15:14:28 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Oct 06 15:39:00 2015 +0200
@@ -502,6 +502,7 @@
val _ = theorem @{command_keyword theorem} false "theorem";
val _ = theorem @{command_keyword lemma} false "lemma";
val _ = theorem @{command_keyword corollary} false "corollary";
+val _ = theorem @{command_keyword proposition} false "proposition";
val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
--- a/src/Pure/Pure.thy Tue Oct 06 15:14:28 2015 +0200
+++ b/src/Pure/Pure.thy Tue Oct 06 15:39:00 2015 +0200
@@ -43,7 +43,7 @@
and "instance" :: thy_goal
and "overloading" :: thy_decl_block
and "code_datatype" :: thy_decl
- and "theorem" "lemma" "corollary" :: thy_goal
+ and "theorem" "lemma" "corollary" "proposition" :: thy_goal
and "schematic_goal" :: thy_goal
and "notepad" :: thy_decl_block
and "have" :: prf_goal % "proof"