summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

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.

--- 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";