little bugfixes; added induct_thm_tac
authoroheimb
Fri Feb 02 00:31:39 2001 +0100 (2001-02-02)
changeset 11029a221d8a9413c
parent 11028 8cf44cbe22e8
child 11030 1b709f59e33a
little bugfixes; added induct_thm_tac
lib/scripts/convert.pl
     1.1 --- a/lib/scripts/convert.pl	Thu Feb 01 21:28:23 2001 +0100
     1.2 +++ b/lib/scripts/convert.pl	Fri Feb 02 00:31:39 2001 +0100
     1.3 @@ -86,8 +86,8 @@
     1.4    s/Asm_simp_tac 1/simp (no_asm_simp)/g;
     1.5    s/Simp_tac 1/simp (no_asm)/g;
     1.6    s/ALLGOALS Asm_full_simp_tac/simp_all/g;
     1.7 -  s/ALLGOALS Full_simp_tac 1/simp_all (no_asm_use)/g;
     1.8 -  s/ALLGOALS Asm_simp_tac 1/simp_all (no_asm_simp)/g;
     1.9 +  s/ALLGOALS Full_simp_tac/simp_all (no_asm_use)/g;
    1.10 +  s/ALLGOALS Asm_simp_tac/simp_all (no_asm_simp)/g;
    1.11    s/ALLGOALS Simp_tac/simp_all (no_asm)/g;
    1.12  
    1.13    s/asm_full_simp_tac \(simpset\(\) (.*?)\) 1/simp $1/g;
    1.14 @@ -119,6 +119,8 @@
    1.15    s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g;
    1.16    s/induct_tac (\".*?\") 1/induct_tac $1/g;
    1.17    s/induct_tac (\".*?\") (\d+)/induct_tac [$2] $1/g;
    1.18 +  s/induct_thm_tac ([\w\'\. \[,\]]+?) (\".*?\") 1/induct_tac $2 rule: $1/g;
    1.19 +  s/induct_thm_tac ([\w\'\. \[,\]]+?) (\".*?\") (\d+)/induct_tac [$3] $2 rule: $1/g;
    1.20    s/subgoal_tac (\".*?\") 1/subgoal_tac $1/g;
    1.21    s/subgoal_tac (\".*?\") (\d+)/subgoal_tac [$2] $1/g;
    1.22    s/thin_tac (\".*?\") *1/erule_tac V = $1 in thin_rl/g;
    1.23 @@ -241,8 +243,7 @@
    1.24    s/^qed *\"(.*?)\"/done($1,"")/se;
    1.25    s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
    1.26    s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_fun($2)/se;
    1.27 -  s/^val *\( *\"(.*?)\" *= *(.*?) *\) *$/"lemmas $1 = ".subst_RS_fun($2)/se;
    1.28 -  s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/"apply$1".process_tac($1,$2).$3/se;
    1.29 +  s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/"apply".$1.process_tac($1,$2).$3/se;
    1.30    s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
    1.31                               # remove outermost parentheses if around atoms
    1.32    s/^Addsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"simp")/seg;