renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
(benchmark Isabelle
:extrasorts ( T2 T1)
:extrafuns (
(uf_2 T1)
(uf_4 T2)
(uf_3 T1)
)
:extrapreds (
(up_1 T1 T2)
)
:assumption (forall (?x1 T1) (?x2 T2) (iff (up_1 ?x1 ?x2) (= ?x1 uf_2)))
:assumption (not (iff (exists (?x3 T2) (up_1 uf_3 ?x3)) (up_1 uf_3 uf_4)))
:formula true
)