src/HOL/Lambda/ROOT.ML
author wenzelm
Wed, 02 Jun 2010 21:12:28 +0200
changeset 37296 1fad5b94c0ae
parent 34205 f69cd974bc4e
child 39126 ee117c5b3b75
permissions -rw-r--r--
replaced ML pokes by explicit usedir -p; prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;

Syntax.ambiguity_level := 100;

no_document use_thys ["Code_Integer"];
use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];