equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 Syntax.ambiguity_level := 100; |
7 Syntax.ambiguity_level := 100; |
8 proofs := 2; |
8 proofs := 2; |
9 |
9 |
10 no_document use_thys ["Accessible_Part", "Pretty_Int"]; |
10 no_document use_thys ["Accessible_Part", "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_thy "WeakNorm"; |