lib/scripts/convert.pl
author oheimb
Mon, 23 Apr 2001 17:11:19 +0200
changeset 11263 e502756bcb11
parent 11198 26a3e549ce8e
child 11271 b2a1d9c20df7
permissions -rw-r--r--
added parentheses for 'b y' syntax, added primitive smp_tac support
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     1
#
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     2
# $Id$
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     3
# Author: David von Oheimb, TU Muenchen
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     4
# License: GPL (GNU GENERAL PUBLIC LICENSE)
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     5
#
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     6
# convert.pl - convert legacy tactic scripts to Isabelle/Isar tactic
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     7
#   emulation using heuristics - leaves unrecognized patterns unchanged
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     8
#   produces from each input file (on the command line) a new file with
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
     9
#   ".thy" appended and renames the original input file by appending "~0~"
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    10
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    11
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    12
sub thmlist {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    13
  my $s = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    14
  $s =~ s/^\[(.*)\]$/$1/sg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    15
  $s =~ s/, +/ /g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    16
  $s =~ s/,/ /g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    17
  $s;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    18
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    19
11014
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    20
sub subst_RS {
11131
5dc3b5abdbca improved subst_RS
oheimb
parents: 11114
diff changeset
    21
  s/ RS ([\w\'\.]+)/ [THEN $1]/g;
5dc3b5abdbca improved subst_RS
oheimb
parents: 11114
diff changeset
    22
  s/ RS \((.+?)\)/ [THEN $1]/g;
5dc3b5abdbca improved subst_RS
oheimb
parents: 11114
diff changeset
    23
  s/\] \[THEN /, /g;
5dc3b5abdbca improved subst_RS
oheimb
parents: 11114
diff changeset
    24
  s/THEN sym\b/symmetric/g;
11014
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    25
}
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    26
11131
5dc3b5abdbca improved subst_RS
oheimb
parents: 11114
diff changeset
    27
sub subst_RS_standard {
11027
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    28
  my $s = shift;
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    29
  $_ = $s;
11131
5dc3b5abdbca improved subst_RS
oheimb
parents: 11114
diff changeset
    30
  s/\s+/ /sg;             # remove multiple whitespace
5dc3b5abdbca improved subst_RS
oheimb
parents: 11114
diff changeset
    31
  s/\s/ /sg;              # substitute all remaining tabs and newlines by space
11027
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    32
  subst_RS();
11131
5dc3b5abdbca improved subst_RS
oheimb
parents: 11114
diff changeset
    33
  s/\]\s*$/, standard]/g;
11027
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    34
  $_;
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    35
}
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    36
11014
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    37
sub decl {
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    38
  my $s = shift;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    39
  my $a = shift;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    40
  $_ = $s;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    41
  subst_RS();
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    42
  s/, */ [$a] /g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    43
  s/$/ [$a]/;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    44
  s/\] *\[/, /g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    45
  "declare $_";
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    46
}
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    47
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    48
sub process_tac {
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    49
  $prefer = "";
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    50
  my $lead = shift;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    51
  my $t = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    52
  my $simpmodmod = ($t =~ m/auto_tac|force_tac|clarsimp_tac/) ? "simp " : "";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    53
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    54
  $_ = $t;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    55
  s/\s+/ /sg;             # remove multiple whitespace
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    56
  s/\s/ /sg;              # substitute all remaining tabs and newlines by space
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    57
  s/\( /\(/g; s/ \)/\)/g; # remove leading and trailing space inside parentheses
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    58
  s/\[ /\[/g; s/ \]/\]/g; # remove leading and trailing space inside sq brackets
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    59
  s/ ?\( ?\)/\(\)/g;      # remove space before and inside empty tuples
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    60
  s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    61
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    62
  s/Blast_tac 1/blast/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    63
  s/^Blast_tac (\d+)/{$prefer="prefer $1 "; "blast"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    64
  s/Fast_tac 1/fast/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    65
  s/^Fast_tac (\d+)/{$prefer="prefer $1 "; "fast"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    66
  s/Slow_tac 1/slow/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    67
  s/^Slow_tac (\d+)/{$prefer="prefer $1 "; "slow"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    68
  s/Best_tac 1/best/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    69
  s/^Best_tac (\d+)/{$prefer="prefer $1 "; "best"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    70
  s/Safe_tac/safe/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    71
  s/Clarify_tac 1/clarify/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    72
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    73
  s/blast_tac \(claset\(\) (.*?)\) 1/blast $1/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    74
  s/^blast_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "blast $1"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    75
  s/fast_tac \(claset\(\) (.*?)\) 1/fast $1/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    76
  s/^fast_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "fast $1"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    77
  s/slow_tac \(claset\(\) (.*?)\) 1/slow $1/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    78
  s/^slow_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "slow $1"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    79
  s/best_tac \(claset\(\) (.*?)\) 1/best $1/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    80
  s/^best_tac \(claset\(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "best $1"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    81
  s/safe_tac \(claset\(\) (.*?)\)/safe $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    82
  s/clarify_tac \(claset\(\) (.*?)\) 1/clarify $1/g;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    83
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    84
  s/Auto_tac/auto/g;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    85
  s/Force_tac 1/force/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    86
  s/^Force_tac (\d+)/{$prefer="prefer $1 "; "force"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    87
  s/Clarsimp_tac 1/clarsimp/g;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    88
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    89
  s/auto_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\)/auto $1 $2/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    90
  s/force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) 1/force $1 $2/g;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
    91
  s/^force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) (\d+)/{$prefer="prefer $3 "; "force $1 $2"}/e;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    92
  s/clarsimp_tac \(claset\(*\) (.*?), *simpset\(\) (.*?)\) 1/clarsimp $1 $2/g;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    93
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    94
  s/Asm_full_simp_tac 1/simp/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    95
  s/Full_simp_tac 1/simp (no_asm_use)/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    96
  s/Asm_simp_tac 1/simp (no_asm_simp)/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    97
  s/Simp_tac 1/simp (no_asm)/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    98
  s/ALLGOALS Asm_full_simp_tac/simp_all/g;
11029
a221d8a9413c little bugfixes; added induct_thm_tac
oheimb
parents: 11027
diff changeset
    99
  s/ALLGOALS Full_simp_tac/simp_all (no_asm_use)/g;
a221d8a9413c little bugfixes; added induct_thm_tac
oheimb
parents: 11027
diff changeset
   100
  s/ALLGOALS Asm_simp_tac/simp_all (no_asm_simp)/g;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   101
  s/ALLGOALS Simp_tac/simp_all (no_asm)/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   102
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   103
  s/asm_full_simp_tac \(simpset\(\) (.*?)\) 1/simp $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   104
  s/full_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_use) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   105
  s/asm_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_simp) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   106
  s/simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   107
  s/ALLGOALS \(asm_full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   108
  s/ALLGOALS \(full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_use) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   109
  s/ALLGOALS \(asm_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_simp) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   110
  s/ALLGOALS \(simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   111
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   112
  s/a(ssume_)?tac 1/assumption/g;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   113
  s/^a(ssume_)?tac (\d+)/{$prefer="prefer $2 "; "assumption"}/e;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   114
  s/\bmp_tac 1/erule (1) notE impE/g;
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   115
  s/\bmp_tac (\d+)/erule_tac [$1] notE impE, tactic \"assume_tac $1\"/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   116
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   117
  s/hypsubst_tac 1/hypsubst/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   118
  s/arith_tac 1/arith/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   119
  s/strip_tac 1/intro strip/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   120
  s/split_all_tac 1/simp (no_asm_simp) only: split_tupled_all/g;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   121
11263
e502756bcb11 added parentheses for 'b y' syntax, added primitive smp_tac support
oheimb
parents: 11198
diff changeset
   122
  s/smp_tac (\d+) (\d+)/tactic "smp_tac $1 $2"/g;
11009
9e0ad9a5f9bb added attribute declarations, etc.
oheimb
parents: 11001
diff changeset
   123
  s/rotate_tac (\d+) (\d+)/rotate_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   124
  s/rotate_tac ~ *(\d+) (\d+)/rotate_tac [$2] -$1/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   125
  s/rename_tac (\".*?\") (\d+)/rename_tac [$2] $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   126
  s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   127
  s/induct_tac (\".*?\") (\d+)/induct_tac [$2] $1/g;
11029
a221d8a9413c little bugfixes; added induct_thm_tac
oheimb
parents: 11027
diff changeset
   128
  s/induct_thm_tac ([\w\'\. \[,\]]+?) (\".*?\") (\d+)/induct_tac [$3] $2 rule: $1/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   129
  s/subgoal_tac (\".*?\") (\d+)/subgoal_tac [$2] $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   130
  s/thin_tac (\".*?\") *(\d+)/erule_tac [$2] V = $1 in thin_rl/g;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   131
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   132
  s/THEN /, /g;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   133
  s/ORELSE/|/g;
11014
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   134
  subst_RS();
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   135
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   136
  s/\(\"(.*?)\" *, *(\".*?\")\) *, */$1 = $2 and /g; # instantiations
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   137
  s/\(\"(.*?)\" *, *(\".*?\")\)/$1 = $2/g;       # last instantiation
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   138
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   139
  s/rewtac ([\w\'\. \[,\]]+)/unfold $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   140
  s/stac ([\w\'\. \[,\]]+?) 1/subst $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   141
  s/rtac ([\w\'\. \[,\]]+?) 1/rule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   142
  s/rtac ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   143
  s/res_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$3] $1 in $2/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   144
  s/dtac ([\w\'\. \[,\]]+?) 1/drule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   145
  s/dtac ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   146
  s/dres_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$3] $1 in $2/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   147
  s/datac ([\w\'\. \[,\]]+?) (\d+) 1/drule ($2) $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   148
  s/etac ([\w\'\. \[,\]]+?) 1/erule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   149
  s/etac ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   150
  s/eres_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$3] $1 in $2/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   151
  s/eatac ([\w\'\. \[,\]]+?) (\d+) 1/erule ($2) $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   152
  s/forward_tac \[([\w\'\. \[,\]]+)\] 1/frule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   153
  s/forward_tac \[([\w\'\. \[,\]]+)\] (\d+)/frule_tac [$2] $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   154
  s/ftac ([\w\'\. \[,\]]+?) 1/frule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   155
  s/ftac ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   156
  s/forw_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$3] $1 in $2/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   157
  s/fatac ([\w\'\. \[,\]]+?) (\d+) 1/frule ($2) $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   158
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   159
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   160
  s/fold_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"fold ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   161
  s/rewrite_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"unfold ".thmlist($1)/eg;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   162
  s/cut_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/cut_tac [$3] $1 in $2/g;
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   163
  s/cut_facts_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) (\d+)/"cut_tac [$2] ".thmlist($1)/eg;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   164
  s/resolve_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) 1/"rule ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   165
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   166
  s/addIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   167
  s/addSIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro!: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   168
  s/addEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   169
  s/addSEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim!: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   170
  s/addDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   171
  s/addSDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest!: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   172
  s/delrules *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"del: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   173
  s/addsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."add: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   174
  s/delsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."del: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   175
  s/addcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong add: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   176
  s/delcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong del: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   177
  s/addsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split add: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   178
  s/delsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split del: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   179
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   180
  s/_tac \[1\]/_tac/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   181
  s/ +/ /g;                       # remove multiple whitespace
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   182
  s/\( /\(/; s/ \)/\)/g;  # remove leading and trailing space inside parentheses
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   183
  s/^ *(.*?) *$/$1/s;             # remove enclosing whitespace
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   184
  s/^([a-zA-Z])/ $1/ if (!($lead =~ m/[\s\(]$/)); # add space if required
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   185
  $prefer."apply".$lead.$_;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   186
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   187
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   188
sub lemmaname { 
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   189
  $lemmanames[++$lemmacount] = "??unknown??"; 
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   190
  "@@" . $lemmacount . "@@"; 
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   191
}
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   192
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   193
sub backpatch_lemmanames {
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   194
  if($currfile ne "") {
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   195
    select(STDOUT);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   196
    close(ARGVOUT);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   197
    open(TMPW, '>'.$finalfile);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   198
    open TMPR,$tmpfile or die "Can't find tmp file $tmp: $!\n";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   199
    while(<TMPR>) {
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   200
      s/@@(\d+)@@/$lemmanames[$1]/eg;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   201
      print TMPW;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   202
    }
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   203
    system("mv $currfile $currfile~0~") if($currfile ne $default);
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   204
    system("rm $tmpfile");
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   205
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   206
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   207
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   208
sub done {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   209
  my $name = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   210
  my $attr = shift;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   211
  $lemmanames[$lemmacount] = $name.$attr;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   212
  "done";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   213
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   214
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   215
$currfile = "";
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   216
$default = "convert_default_stdout";
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   217
while (<>) { # main loop
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   218
  if ($ARGV ne $currfile) {
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   219
    $x=$_; backpatch_lemmanames; $_=$x;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   220
    $currfile = ($ARGV eq "-" ? $default : $ARGV);
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   221
    $lemmacount=0;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   222
    $finalfile = "$currfile.thy";
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   223
    $tmpfile   = "$finalfile.~0~";
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   224
    open(ARGVOUT, '>'.$tmpfile);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   225
    select(ARGVOUT);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   226
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   227
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   228
 nl:
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   229
  if(!s/;(\s*?(\n?$|\(\*))/$1/s && !eof()) {# no end_of_ML_command marker
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   230
    $_ = $_ . <>;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   231
    goto nl;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   232
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   233
  s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   234
 nlc:
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   235
  m/^(\s*)(.*?)(\s*)$/s;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   236
  $head=$1; $line=$2; $tail=$3;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   237
  $tail =~ s/\s+\n/\n/sg;  # remove trailing whitespace at end of lines
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   238
  print $head; $_=$line.$tail;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   239
  if ($line =~ m/^\(\*/) { # start comment
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   240
    while (($i = index $_,"*)") == -1 && !eof()) { # no end comment
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   241
      print;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   242
      $_ = <>;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   243
    }
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   244
    if ($i == -1) { print; last; } 
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   245
    print substr $_,0,$i+2;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   246
    $_ = substr $_,$i+2;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   247
    goto nlc;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   248
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   249
  $_=$line;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   250
  s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\. \[,\]]+) *(.+)/
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   251
    "lemma ".lemmaname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   252
  s/^Goal *(.+)/"lemma ".lemmaname().": $1"/se;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   253
  s/\bgoal/"(*".lemmaname()."*)goal"/se; # ugly old-style goals
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   254
  s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   255
  s/^qed *\"(.*?)\"/done($1,"")/se;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   256
  s/^val *(\w+) *= *result *\( *\) *$/done($1,"")/se;
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   257
  s/^bind_thm *\( *\"(.*?)\" *, *(result *\( *\) *?) *\) *$/done($1,"")/se;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   258
  s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
11131
5dc3b5abdbca improved subst_RS
oheimb
parents: 11114
diff changeset
   259
  s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_standard($2)/se;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   260
  s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/process_tac($1,$2).$3/se;
11263
e502756bcb11 added parentheses for 'b y' syntax, added primitive smp_tac support
oheimb
parents: 11198
diff changeset
   261
  s/^b\s+y(\s*)(.*?)(\s*)$/process_tac($1,"(".$2.")").$3/se;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   262
  s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   263
                             # remove outermost parentheses if around atoms
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   264
  s/^Addsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp")/seg;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   265
  s/^Delsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp del")/seg;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   266
  s/^Addsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split")/seg;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   267
  s/^Delsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split del")/seg;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   268
  s/^AddIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro")/seg;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   269
  s/^AddSIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro!")/seg;
11114
a0c3f2082c88 added support for AddXIs, AddXEs, AddXDs
oheimb
parents: 11081
diff changeset
   270
  s/^AddXIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro?")/seg;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   271
  s/^AddEs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"elim")/seg;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   272
  s/^AddSEs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"elim!")/seg;
11114
a0c3f2082c88 added support for AddXIs, AddXEs, AddXDs
oheimb
parents: 11081
diff changeset
   273
  s/^AddXEs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"elim?")/seg;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   274
  s/^AddDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest")/seg;
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   275
  s/^AddSDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest!")/seg;
11114
a0c3f2082c88 added support for AddXIs, AddXEs, AddXDs
oheimb
parents: 11081
diff changeset
   276
  s/^AddXDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest?")/seg;
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   277
  s/^AddIffs\s*\[?\s*([\w\'\. ,]*)\s*\]?</decl($1,"iff")/seg;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   278
  print "$_$tail";
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   279
  if(eof()) { last; } # prevents reading finally from stdin (thru <>)!
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   280
}
11081
ce9a6746cd1e solved non-initialization problems; improvements using prefer
oheimb
parents: 11068
diff changeset
   281
backpatch_lemmanames;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   282
select(STDOUT);