From 6ff59c83de9ce7d5715fae19f50d94b0b973414a Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 28 May 2020 14:07:52 +0200
Subject: case distinction

---
 spartan/core/Spartan.thy | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'spartan/core/Spartan.thy')

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' (
-- 
cgit v1.2.3