author | krauss |
Fri, 25 Apr 2008 15:30:33 +0200 | |
changeset 26748 | 4d51ddd6aa5c |
parent 25374 | 7657a081fcb4 |
child 33615 | 261abc2e3155 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Lambda/ROOT.ML |
1126 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
5261
ce3c25c8a694
First steps towards termination of simply typed terms.
nipkow
parents:
1465
diff
changeset
|
4 |
Copyright 1998 TUM |
1126 | 5 |
*) |
6 |
||
11943 | 7 |
Syntax.ambiguity_level := 100; |
25374 | 8 |
Proofterm.proofs := 2; |
11943 | 9 |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
25374
diff
changeset
|
10 |
no_document use_thys ["Code_Integer"]; |
24535 | 11 |
use_thys ["Eta", "StrongNorm", "Standardization"]; |
14090
f24b2818c1e7
Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been
berghofe
parents:
14067
diff
changeset
|
12 |
if HOL_proofs < 2 then |
f24b2818c1e7
Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been
berghofe
parents:
14067
diff
changeset
|
13 |
warning "HOL proof terms required for running theory WeakNorm" |
21676 | 14 |
else use_thy "WeakNorm"; |