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

author | wenzelm |

Tue, 06 Oct 2015 15:39:00 +0200 | |

changeset 61338 | de610e8df459 |

parent 61337 | 4645502c3c64 |

child 61339 | 93883c825062 |

added 'proposition' command;

NEWS | file | annotate | diff | comparison | revisions | |

src/Doc/Isar_Ref/Proof.thy | file | annotate | diff | comparison | revisions | |

src/Pure/Isar/isar_syn.ML | file | annotate | diff | comparison | revisions | |

src/Pure/Pure.thy | file | annotate | diff | comparison | revisions |

--- 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"