equal
deleted
inserted
replaced
113 val _ = warning (PolyML.makestring phis) |
113 val _ = warning (PolyML.makestring phis) |
114 val _ = app (warning o Syntax.string_of_term @{context}) ts |
114 val _ = app (warning o Syntax.string_of_term @{context}) ts |
115 *) |
115 *) |
116 val state = Proof.init @{context} |
116 val state = Proof.init @{context} |
117 val params = |
117 val params = |
118 [("card", "1\<emdash>8"), |
118 [("card iota", "1\<emdash>100"), |
|
119 ("card", "1\<emdash>8"), |
119 ("box", "false"), |
120 ("box", "false"), |
120 ("sat_solver", "smart"), |
121 ("sat_solver", "smart"), |
121 ("max_threads", "1"), |
122 ("max_threads", "1"), |
122 ("batch_size", "10"), |
123 ("batch_size", "10"), |
123 (* ("debug", "true"), *) |
124 (* ("debug", "true"), *) |