diff options
Diffstat (limited to '')
-rw-r--r-- | spartan/core/Spartan.thy | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 4e53a45..b0fec5a 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -162,7 +162,8 @@ ML_file \<open>lib/congruence.ML\<close> section \<open>Methods\<close> -ML_file \<open>lib/elimination.ML\<close> \<comment> \<open>declares the [elims] attribute\<close> +ML_file \<open>lib/elimination.ML\<close> \<comment> \<open>elimination rules\<close> +ML_file \<open>lib/cases.ML\<close> \<comment> \<open>case reasoning rules\<close> named_theorems intros and comps lemmas @@ -194,6 +195,9 @@ method_setup elim = method elims = elim+ +method_setup cases = + \<open>Args.term >> (fn tm => fn ctxt => SIMPLE_METHOD' (cases_tac tm ctxt))\<close> + (*This could possibly use additional simplification hints via a simp: modifier*) method_setup typechk = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' ( |