On Thu, 26 Apr 2012, Christian Sternagel wrote:
Referring to
http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_25-Apr-2012_bundle_x86_64-linux.tar.gz
When calling
./bin/isabelle mirabelle
I obtain
...
Available OPTIONs for the ACTION sledgehammer:
grep:
/home/griff/Downloads/Isabelle_25-Apr-2012/src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML:
No such file or directory
I have amended this in Isabelle/bbc3e7bccc61 -- I was partly responsible
for the confusion of Nik Sultana here.
I have also made the shell script a bit more robust in 030d3c89eacf,
hopefully without breaking it.
I was just curious what "mirabelle" actually is/does, which I still
don't know.
I don't know how (or if) it is tested.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
