doc-src/TutorialI/IsarOverview/Isar/makeDemo

- eliminated thin_leading_eqs_tac
- gen_hyp_subst_tac now uses asm_lr_simp_tac instead of asm_full_simp_tac,
in order to avoid divergence of new simplifier

#!/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"; }
}