Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been
authorberghofe
Fri, 04 Jul 2003 17:09:26 +0200
changeset 14090 f24b2818c1e7
parent 14089 7b34f58b1b81
child 14091 ad6ba9c55190
Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been compiled without proof objects.
src/HOL/Lambda/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lambda/ROOT.ML	Thu Jul 03 18:07:50 2003 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Fri Jul 04 17:09:26 2003 +0200
@@ -12,4 +12,6 @@
 time_use_thy "Eta";
 no_document time_use_thy "Accessible_Part";
 time_use_thy "StrongNorm";
-time_use_thy "WeakNorm";
+if HOL_proofs < 2 then
+  warning "HOL proof terms required for running theory WeakNorm"
+else time_use_thy "WeakNorm";
isabelle