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