diff options
author | Josh Chen | 2020-07-08 15:55:48 +0200 |
---|---|---|
committer | Josh Chen | 2020-07-08 15:55:48 +0200 |
commit | 07c51b1801bd701bef61cedd571a944d9bd37e8b (patch) | |
tree | 16b9581f9f52af4058594cd503aa2eec1d2cb801 /spartan/core/goals.ML | |
parent | f0fab6e197510ce0e6d23a669f69de966701d495 (diff) |
1. Initial `Definition` keyword. 2. ifelse.
Diffstat (limited to '')
-rw-r--r-- | spartan/core/goals.ML | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML index 9f394f0..4b53a7f 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/goals.ML @@ -204,11 +204,20 @@ fun theorem spec descr = schematic_theorem_cmd (case opt_derive of SOME "derive" => true | _ => false) long descr NONE (K I) binding includes elems concl)) + +fun definition spec descr = + Outer_Syntax.local_theory_to_proof' spec "definition via proof" + ((long_statement || short_statement) >> + (fn (long, binding, includes, elems, concl) => schematic_theorem_cmd + true long descr NONE (K I) binding includes elems concl)) + + in val _ = theorem \<^command_keyword>\<open>Theorem\<close> "Theorem" val _ = theorem \<^command_keyword>\<open>Lemma\<close> "Lemma" val _ = theorem \<^command_keyword>\<open>Corollary\<close> "Corollary" val _ = theorem \<^command_keyword>\<open>Proposition\<close> "Proposition" +val _ = definition \<^command_keyword>\<open>Definition\<close> "Definition" end |