# HG changeset patch
# User paulson
# Date 1061370257 -7200
# Node ID 2072802ab0e385096d63f053a8dd87d0250bd0df
# Parent  0a26b15b42c6eebebb263f98855ec7a296ff0107
new case_tac method

diff -r 0a26b15b42c6 -r 2072802ab0e3 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Wed Aug 20 11:00:37 2003 +0200
+++ b/src/FOL/FOL.thy	Wed Aug 20 11:04:17 2003 +0200
@@ -24,7 +24,8 @@
 
 use "cladata.ML"
 setup Cla.setup
-setup clasetup
+setup cla_setup
+setup case_setup
 
 use "blastdata.ML"
 setup Blast.setup
diff -r 0a26b15b42c6 -r 2072802ab0e3 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Wed Aug 20 11:00:37 2003 +0200
+++ b/src/FOL/cladata.ML	Wed Aug 20 11:04:17 2003 +0200
@@ -50,4 +50,9 @@
 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
                      addSEs [exE,alt_ex1E] addEs [allE];
 
-val clasetup = [fn thy => (claset_ref_of thy := FOL_cs; thy)];
+val cla_setup = [fn thy => (claset_ref_of thy := FOL_cs; thy)];
+
+val case_setup =
+ [Method.add_methods
+    [("case_tac", Method.goal_args Args.name case_tac,
+      "case_tac emulation (dynamic instantiation!)")]];