| author | haftmann |
| Wed, 07 Oct 2009 14:01:26 +0200 | |
| changeset 32887 | 85e7ab9020ba |
| parent 26748 | 4d51ddd6aa5c |
| child 33615 | 261abc2e3155 |
| permissions | -rw-r--r-- |
(* Title: HOL/Lambda/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM *) Syntax.ambiguity_level := 100; Proofterm.proofs := 2; no_document use_thys ["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";