| changeset 33615 | 261abc2e3155 |
| parent 26748 | 4d51ddd6aa5c |
| child 34205 | f69cd974bc4e |
| 33608:5c0024338cef | 33615:261abc2e3155 |
|---|---|
9 |
9 |
10 no_document use_thys ["Code_Integer"]; |
10 no_document use_thys ["Code_Integer"]; |
11 use_thys ["Eta", "StrongNorm", "Standardization"]; |
11 use_thys ["Eta", "StrongNorm", "Standardization"]; |
12 if HOL_proofs < 2 then |
12 if HOL_proofs < 2 then |
13 warning "HOL proof terms required for running theory WeakNorm" |
13 warning "HOL proof terms required for running theory WeakNorm" |
14 else use_thy "WeakNorm"; |
14 else use_thys ["WeakNorm"]; |