| author | haftmann |
| Tue, 30 Oct 2007 08:45:55 +0100 | |
| changeset 25231 | 1aa9c8f022d0 |
| parent 24994 | c385c4eabb3b |
| child 25374 | 7657a081fcb4 |
| permissions | -rw-r--r-- |
(* Title: HOL/Lambda/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM *) Syntax.ambiguity_level := 100; proofs := 2; no_document use_thys ["Accessible_Part", "Code_Integer"]; use_thys ["Eta", "StrongNorm", "Standardization"]; if HOL_proofs < 2 then warning "HOL proof terms required for running theory WeakNorm" else use_thy "WeakNorm";