| author | blanchet |
| Fri, 11 Jun 2010 17:10:23 +0200 | |
| changeset 37399 | 34f080a12063 |
| parent 37296 | 1fad5b94c0ae |
| child 39126 | ee117c5b3b75 |
| permissions | -rw-r--r-- |
| 11943 | 1 |
Syntax.ambiguity_level := 100; |
2 |
||
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
25374
diff
changeset
|
3 |
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
|
4 |
use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"]; |