equal
deleted
inserted
replaced
12 "Eval_Examples", |
12 "Eval_Examples", |
13 "Quickcheck", |
13 "Quickcheck", |
14 "Term_Of_Syntax", |
14 "Term_Of_Syntax", |
15 "Codegenerator", |
15 "Codegenerator", |
16 "Codegenerator_Pretty", |
16 "Codegenerator_Pretty", |
17 "NormalForm" |
17 "NormalForm", |
|
18 "../NumberTheory/Factorization", |
|
19 "../Library/BigO" |
18 ]; |
20 ]; |
19 |
21 |
20 use_thys [ |
22 use_thys [ |
21 "Numeral", |
23 "Numeral", |
22 "ImperativeQuicksort", |
24 "ImperativeQuicksort", |
60 "Coherent", |
62 "Coherent", |
61 "Dense_Linear_Order_Ex", |
63 "Dense_Linear_Order_Ex", |
62 "PresburgerEx", |
64 "PresburgerEx", |
63 "Reflected_Presburger", |
65 "Reflected_Presburger", |
64 "Reflection", |
66 "Reflection", |
65 "ReflectionEx" |
67 "ReflectionEx", |
|
68 "BinEx", |
|
69 "Sqrt", |
|
70 "Sqrt_Script", |
|
71 "BigO_Complex", |
|
72 "Arithmetic_Series_Complex", |
|
73 "HarmonicSeries", |
|
74 "MIR", |
|
75 "ReflectedFerrack", |
|
76 "Refute_Examples", |
|
77 "Quickcheck_Examples" |
66 ]; |
78 ]; |
67 |
79 |
68 setmp Proofterm.proofs 2 use_thy "Hilbert_Classical"; |
80 setmp Proofterm.proofs 2 use_thy "Hilbert_Classical"; |
69 |
81 |
70 |
82 |
71 use_thy "SVC_Oracle"; |
83 use_thy "SVC_Oracle"; |
72 |
84 |
73 fun svc_enabled () = getenv "SVC_HOME" <> ""; |
85 fun svc_enabled () = getenv "SVC_HOME" <> ""; |
74 fun if_svc_enabled f x = if svc_enabled () then f x else (); |
86 fun if_svc_enabled f x = if svc_enabled () then f x else (); |
75 |
87 |
76 if_svc_enabled time_use_thy "svc_test"; |
88 if_svc_enabled use_thy "svc_test"; |
77 |
89 |
78 |
90 |
79 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *) |
91 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *) |
80 (* installed: *) |
92 (* installed: *) |
81 try use_thy "SAT_Examples"; |
93 try use_thy "SAT_Examples"; |
84 (* installed: *) |
96 (* installed: *) |
85 if getenv "ZCHAFF_HOME" <> "" then |
97 if getenv "ZCHAFF_HOME" <> "" then |
86 use_thy "Sudoku" |
98 use_thy "Sudoku" |
87 else (); |
99 else (); |
88 |
100 |
89 time_use_thy "Refute_Examples"; |
|
90 time_use_thy "Quickcheck_Examples"; |
|
91 |
|
92 HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"]; |
101 HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"]; |
93 |
|
94 no_document use_thys [ |
|
95 "../NumberTheory/Factorization", |
|
96 "../Library/BigO" |
|
97 ]; |
|
98 |
|
99 use_thys [ |
|
100 "BinEx", |
|
101 "Sqrt", |
|
102 "Sqrt_Script", |
|
103 "BigO_Complex", |
|
104 |
|
105 "Arithmetic_Series_Complex", |
|
106 "HarmonicSeries", |
|
107 |
|
108 "MIR", |
|
109 "ReflectedFerrack" |
|
110 ]; |
|
111 |
|