# HG changeset patch
# User paulson
# Date 903351989 -7200
# Node ID ec84178243ffc6e88b9b20b96906afe6bc6aa949
# Parent  028e00595280765f9e48277187b814845e7bbc8d
Now allows "." in rule names, with special treatment for "be"

diff -r 028e00595280 -r ec84178243ff lib/scripts/expandshort.pl
--- a/lib/scripts/expandshort.pl	Mon Aug 17 11:00:57 1998 +0200
+++ b/lib/scripts/expandshort.pl	Mon Aug 17 13:06:29 1998 +0200
@@ -5,6 +5,7 @@
 #
 # in "be ... i;" -> "by (etac ... i);" the "..." phrase is not allowed to
 #   contain punctuation.  Otherwise, comments can be affected!
+# a special case is made to detect    be alpha.alpha digits   
 
 sub expandshort {
     my ($file) = @_;
@@ -20,14 +21,15 @@
     s/ *\(Safe_tac\)/ Safe_tac/sg;
     s/\bby\(/by (/sg;
     s/\bba\b *(\d+);/by (assume_tac $1);/sg;
-    s/\bbr\b *([^;.*!]*) (\d+);/by (rtac $1 $2);/sg;
-    s/\bbrs\b *([^;.*!]*) (\d+);/by (resolve_tac $1 $2);/sg;
-    s/\bbd\b *([^;.*!]*) (\d+);/by (dtac $1 $2);/sg;
-    s/\bbds\b *([^;.*!]*) (\d+);/by (dresolve_tac $1 $2);/sg;
+    s/\bbr\b *([^;*!]*) (\d+);/by (rtac $1 $2);/sg;
+    s/\bbrs\b *([^;*!]*) (\d+);/by (resolve_tac $1 $2);/sg;
+    s/\bbd\b *([^;*!]*) (\d+);/by (dtac $1 $2);/sg;
+    s/\bbds\b *([^;*!]*) (\d+);/by (dresolve_tac $1 $2);/sg;
     s/\bbe\b *([^;.*!]*) (\d+);/by (etac $1 $2);/sg;
-    s/\bbes\b *([^;.*!]*) (\d+);/by (eresolve_tac $1 $2);/sg;
-    s/\bbw\b *([^;.*!]*);/by (rewtac $1);/sg;
-    s/\bbws\b *([^;.*!]*);/by (rewrite_goals_tac $1);/sg;
+    s/\bbe\b *(\w+\.\w+) (\d+);/by (etac $1 $2);/sg;
+    s/\bbes\b *([^;*!]*) (\d+);/by (eresolve_tac $1 $2);/sg;
+    s/\bbw\b *([^;*!]*);/by (rewtac $1);/sg;
+    s/\bbws\b *([^;*!]*);/by (rewrite_goals_tac $1);/sg;
     s/\bauto *\(\)/by Auto_tac/sg;
     s/dresolve_tac *\[(\w+)\] */dtac $1 /sg;
     s/eresolve_tac *\[(\w+)\] */etac $1 /sg;