author | wenzelm |
Tue, 29 Dec 2009 16:20:39 +0100 | |
changeset 34205 | f69cd974bc4e |
parent 33615 | 261abc2e3155 |
child 37296 | 1fad5b94c0ae |
permissions | -rw-r--r-- |
11943 | 1 |
Syntax.ambiguity_level := 100; |
25374 | 2 |
Proofterm.proofs := 2; |
11943 | 3 |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
25374
diff
changeset
|
4 |
no_document use_thys ["Code_Integer"]; |
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
33615
diff
changeset
|
5 |
use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"]; |