replaced exhaust_tac by case_tac;
authorwenzelm
Mon, 13 Mar 2000 16:24:52 +0100
changeset 8444 8f8eb220d9aa
parent 8443 0ed4b608ba4b
child 8445 86e99f863932
replaced exhaust_tac by case_tac;
lib/scripts/fixdatatype.pl
--- a/lib/scripts/fixdatatype.pl	Mon Mar 13 16:24:23 2000 +0100
+++ b/lib/scripts/fixdatatype.pl	Mon Mar 13 16:24:52 2000 +0100
@@ -23,8 +23,8 @@
     ## replace specific induct_tac by generic induct_tac
     s/[\w\.]+\.induct_tac/induct_tac/sg;
 
-    ## replace res_inst_tac ... natE by exhaust_tac
-    s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/exhaust_tac $1/sg;
+    ## replace res_inst_tac ... natE by case_tac
+    s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/case_tac $1/sg;
 
     $result = $_;