equal
deleted
inserted
replaced
31 val thys = [@{theory List}] |
31 val thys = [@{theory List}] |
32 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
32 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
33 val prover = hd provers |
33 val prover = hd provers |
34 val range = (1, NONE) |
34 val range = (1, NONE) |
35 val step = 1 |
35 val step = 1 |
|
36 val linearize = false |
36 val max_suggestions = 1024 |
37 val max_suggestions = 1024 |
37 val dir = "List" |
38 val dir = "List" |
38 val prefix = "/tmp/" ^ dir ^ "/" |
39 val prefix = "/tmp/" ^ dir ^ "/" |
39 *} |
40 *} |
40 |
41 |
45 () |
46 () |
46 *} |
47 *} |
47 |
48 |
48 ML {* |
49 ML {* |
49 if do_it then |
50 if do_it then |
50 generate_accessibility @{context} thys false (prefix ^ "mash_accessibility") |
51 generate_accessibility @{context} thys linearize |
|
52 (prefix ^ "mash_accessibility") |
51 else |
53 else |
52 () |
54 () |
53 *} |
55 *} |
54 |
56 |
55 ML {* |
57 ML {* |
56 if do_it then |
58 if do_it then |
57 generate_features @{context} prover thys false (prefix ^ "mash_features") |
59 generate_features @{context} prover thys (prefix ^ "mash_features") |
58 else |
60 else |
59 () |
61 () |
60 *} |
62 *} |
61 |
63 |
62 ML {* |
64 ML {* |
63 if do_it then |
65 if do_it then |
64 generate_isar_dependencies @{context} thys false |
66 generate_isar_dependencies @{context} thys linearize |
65 (prefix ^ "mash_dependencies") |
67 (prefix ^ "mash_dependencies") |
66 else |
68 else |
67 () |
69 () |
68 *} |
70 *} |
69 |
71 |
70 ML {* |
72 ML {* |
71 if do_it then |
73 if do_it then |
72 generate_isar_commands @{context} prover (range, step) thys |
74 generate_isar_commands @{context} prover (range, step) thys |
73 (prefix ^ "mash_commands") |
75 linearize (prefix ^ "mash_commands") |
74 else |
76 else |
75 () |
77 () |
76 *} |
78 *} |
77 |
79 |
78 ML {* |
80 ML {* |
79 if do_it then |
81 if do_it then |
80 generate_mepo_suggestions @{context} params (range, step) thys |
82 generate_mepo_suggestions @{context} params (range, step) thys |
81 max_suggestions (prefix ^ "mepo_suggestions") |
83 linearize max_suggestions (prefix ^ "mepo_suggestions") |
82 else |
84 else |
83 () |
85 () |
84 *} |
86 *} |
85 |
87 |
86 ML {* |
88 ML {* |
91 () |
93 () |
92 *} |
94 *} |
93 |
95 |
94 ML {* |
96 ML {* |
95 if do_it then |
97 if do_it then |
96 generate_prover_dependencies @{context} params range thys false |
98 generate_prover_dependencies @{context} params range thys linearize |
97 (prefix ^ "mash_prover_dependencies") |
99 (prefix ^ "mash_prover_dependencies") |
98 else |
100 else |
99 () |
101 () |
100 *} |
102 *} |
101 |
103 |
102 ML {* |
104 ML {* |
103 if do_it then |
105 if do_it then |
104 generate_prover_commands @{context} params (range, step) thys |
106 generate_prover_commands @{context} params (range, step) thys |
105 (prefix ^ "mash_prover_commands") |
107 linearize (prefix ^ "mash_prover_commands") |
106 else |
108 else |
107 () |
109 () |
108 *} |
110 *} |
109 |
111 |
110 ML {* |
112 ML {* |