add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
#!/usr/bin/env perl
#
# Author: Makarius
#
# bash - invoke shell command line (with robust signal handling)
#
use warnings;
use strict;
# args
my ($group, $script_name, $pid_name, $output_name) = @ARGV;
# process id
if ($group eq "group") {
use POSIX "setsid";
POSIX::setsid || die $!;
}
open (PID_FILE, ">", $pid_name) || die $!;
print PID_FILE "$$";
close PID_FILE;
# exec script
exec qq/exec bash '$script_name' > '$output_name'/;