author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 14090 | f24b2818c1e7 |
child 21676 | a45af03f6827 |
permissions | -rw-r--r-- |
(* Title: HOL/Lambda/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM *) Syntax.ambiguity_level := 100; proofs := 2; IsarOutput.modes := "no_brackets" :: !IsarOutput.modes; set timing; time_use_thy "Eta"; no_document time_use_thy "Accessible_Part"; time_use_thy "StrongNorm"; if HOL_proofs < 2 then warning "HOL proof terms required for running theory WeakNorm" else time_use_thy "WeakNorm";