equal
deleted
inserted
replaced
80 |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop) |
80 |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop) |
81 o ATP_Util.unextensionalize_def) |
81 o ATP_Util.unextensionalize_def) |
82 val nondefs = pseudo_defs @ nondefs |
82 val nondefs = pseudo_defs @ nondefs |
83 val state = Proof.init ctxt |
83 val state = Proof.init ctxt |
84 val params = |
84 val params = |
85 [("card", "1\<emdash>100"), |
85 [("card", "1-100"), |
86 ("box", "false"), |
86 ("box", "false"), |
87 ("max_threads", "1"), |
87 ("max_threads", "1"), |
88 ("batch_size", "5"), |
88 ("batch_size", "5"), |
89 ("falsify", if null conjs then "false" else "true"), |
89 ("falsify", if null conjs then "false" else "true"), |
90 ("verbose", "true"), |
90 ("verbose", "true"), |