diff options
| author | Josh Chen | 2020-05-28 14:07:52 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-28 14:07:52 +0200 |
| commit | 6ff59c83de9ce7d5715fae19f50d94b0b973414a (patch) | |
| tree | e9a677840721ed6a38d3edb159061b258b4c8ccf /spartan/core/Spartan.thy | |
| parent | a9606c980dcc32ade28ebd1515cad33b380ebd64 (diff) | |
case distinction
Diffstat (limited to 'spartan/core/Spartan.thy')
| -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' ( |