adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Isabelle2017: update AutoCorresTest for RC1 

Add a "sessions" section to the AutoCorresTest ROOT file, to allow
the IsPrime test to import from HOL-Number_Theory.
This commit is contained in:
Matthew Brecknell 2017-09-11 16:24:31 +10:00
parent 379fafe084
commit f8bf97f4e3
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tools/autocorres/Makefile
View File

@ -25,7 +25,7 @@ tests/ROOT: \
tests/examples/*.c \
tests/examples/*.thy \
../../misc/scripts/gen_isabelle_root.py
python ../../misc/scripts/gen_isabelle_root.py -o $@ -b AutoCorres -s AutoCorresTest \
python ../../misc/scripts/gen_isabelle_root.py -o $@ -b AutoCorres -s AutoCorresTest -d HOL-Number_Theory \
-i tests/parse-tests -i tests/proof-tests -i tests/examples --quick-and-dirty
# Generate a Isabelle "All.thy" file containing imports to all the test cases.