| changeset 60190 | 906de96ba68a |
| parent 60094 | 96a4765ba7d1 |
| child 60275 | d8a4fe35da00 |
| 60189:0d3a62127057 | 60190:906de96ba68a |
|---|---|
152 end; |
152 end; |
153 |
153 |
154 fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt; |
154 fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt; |
155 |
155 |
156 fun try0_trans quad = |
156 fun try0_trans quad = |
157 Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of); |
157 Toplevel.keep_proof |
158 (ignore o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of); |
|
158 |
159 |
159 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2); |
160 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2); |
160 |
161 |
161 fun string_of_xthm (xref, args) = |
162 fun string_of_xthm (xref, args) = |
162 Facts.string_of_ref xref ^ |
163 Facts.string_of_ref xref ^ |