diff options
| author | Josh Chen | 2020-05-22 15:43:14 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-22 15:43:14 +0200 |
| commit | 720da0f918118388d114e09664b129d2b29be2b1 (patch) | |
| tree | e4411cceae3a790544e7bebb4eb7717c31e0fa63 /spartan/theories/Spartan.thy | |
| parent | 1571e03b7dc5c7e6f2a46be57a12dd0d25fea452 (diff) | |
some tweaks and comments, in preparation for general inductive type elimination
Diffstat (limited to 'spartan/theories/Spartan.thy')
| -rw-r--r-- | spartan/theories/Spartan.thy | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy index a79f209..5274ea2 100644 --- a/spartan/theories/Spartan.thy +++ b/spartan/theories/Spartan.thy @@ -8,7 +8,7 @@ imports keywords "Theorem" "Lemma" "Corollary" "Proposition" :: thy_goal_stmt and "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and - "derive" "vars":: quasi_command and + "derive" "prems" "vars":: quasi_command and "print_coercions" :: thy_decl begin @@ -138,9 +138,6 @@ axiomatization where \<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x" - - - section \<open>Proof commands\<close> named_theorems typechk @@ -152,6 +149,7 @@ ML_file \<open>../lib/focus.ML\<close> section \<open>Congruence automation\<close> +(*Work in progress*) ML_file \<open>../lib/congruence.ML\<close> @@ -188,6 +186,7 @@ method_setup elim = method elims = elim+ +(*This could possibly use additional simplification hints via a simp: modifier*) method_setup typechk = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD ( CHANGED (ALLGOALS (TRY o typechk_tac ctxt))))\<close> |