spechub/Hets — pull request #1290 by cmaeder (2014-07-17 14:24:38+00:00)
Title: 1284 isabelle batch prover

This batch prover expects a matching .thy file containing the proofs (like RCCVerification_RCC_FO_in_MetricSpace__T.thy) to lie around. A usable .hpf file could contain:

```
use Calculi/Space/RCCVerification
dg-all auto
dg basic RCC_FO_in_MetricSpace__T
prover isabelle-process
prove
```

Currently all theorems of a node must be proven together. A time limit is ignored (but checking is fast).
For batch proving there is no difference between the prover "Isabelle" and "isabelle-process". Only in interactive GUI mode "Isabelle" pops up an emacs whereas "isabelle-process" runs as in batch mode (without user interaction).