equal
deleted
inserted
replaced
21 s/\bprimrec\b\s+([\w]+|"[^"]+")\s+([\w\.]+)/primrec/sg; |
21 s/\bprimrec\b\s+([\w]+|"[^"]+")\s+([\w\.]+)/primrec/sg; |
22 |
22 |
23 ## replace specific induct_tac by generic induct_tac |
23 ## replace specific induct_tac by generic induct_tac |
24 s/[\w\.]+\.induct_tac/induct_tac/sg; |
24 s/[\w\.]+\.induct_tac/induct_tac/sg; |
25 |
25 |
26 ## replace res_inst_tac ... natE by exhaust_tac |
26 ## replace res_inst_tac ... natE by case_tac |
27 s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/exhaust_tac $1/sg; |
27 s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/case_tac $1/sg; |
28 |
28 |
29 $result = $_; |
29 $result = $_; |
30 |
30 |
31 if ($text ne $result) { |
31 if ($text ne $result) { |
32 print STDERR "fixing $file\n"; |
32 print STDERR "fixing $file\n"; |