doc-src/TutorialI/Overview/LNCS/makeDemo

- deleted unneeded function eta_long (now in Pure/pattern.ML
- added HOL.min / HOL.max to allowed consts again
- added final simplification step with presburger_ss to
preprocessor again

#!/usr/bin/perl -w

sub doit {
    my ($file) = @_;

    open (FILE, $file) || die $!;
    undef $/; $text = <FILE>; $/ = "\n";
    close FILE || die $!;

    $_ = $text;

    s/text_raw\{\*([^*]|\*[^}])*\*\}//sg;       # actual work done here
    s/text\{\*([^*]|\*[^}])*\*\}//sg;       # actual work done here
    s/\(\*<\*\)//sg;
    s/\(\*>\*\)//sg;

    $result = $_;

    if ($text ne $result) {
        print STDERR "fixing $file\n";
#        if (! -f "$file~~") {
#            rename $file, "$file~~" || die $!;
#        }
        open (FILE, "> Demo/$file") || die $!;
        print FILE $result;
        close FILE || die $!;
    }
}


foreach $file (@ARGV) {
  eval { &doit($file); };
  if ($@) { print STDERR "*** doit $file: ", $@, "\n"; }
}