author | wenzelm |
Tue, 04 Nov 1997 09:27:32 +0100 | |
changeset 4110 | d7c963600bda |
parent 4109 | b131edcfeac3 |
child 4111 | 93baba60ece2 |
--- a/lib/scripts/fixclasimp.pl Tue Nov 04 09:26:15 1997 +0100 +++ b/lib/scripts/fixclasimp.pl Tue Nov 04 09:27:32 1997 +0100 @@ -13,7 +13,7 @@ $_ = $text; - s/set_current_thy\s"([^"]*)"/context $1.thy/sg; + s/set_current_thy\s*"([^"]*)"/context $1.thy/sg; s/!\s*simpset/simpset()/sg; s/simpset\s*:=/simpset_ref() :=/sg;