# HG changeset patch
# User wenzelm
# Date 1444138740 -7200
# Node ID de610e8df459caad44b29040b40d63b875d782ac
# Parent  4645502c3c64bbf96a17ea3af2ba5b53e95d4801
added 'proposition' command;

diff -r 4645502c3c64 -r de610e8df459 NEWS
--- 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 ***
 
diff -r 4645502c3c64 -r de610e8df459 src/Doc/Isar_Ref/Proof.thy
--- 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.
diff -r 4645502c3c64 -r de610e8df459 src/Pure/Isar/isar_syn.ML
--- 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";
 
 
diff -r 4645502c3c64 -r de610e8df459 src/Pure/Pure.thy
--- 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"