diff --git a/.ocamlformat b/.ocamlformat
index 7d1da85f551dcf95be16a036b13a6672d8e57a72..f4273f4d43843fefc1021bdf3c01fd8d1194fcb8 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,4 +1,4 @@
-version=0.22.4
+version=0.23.0
 exp-grouping=parens
 if-then-else=keyword-first
 max-indent=2
diff --git a/doc/mnist.rst b/doc/mnist.rst
index cee05c3aaf468ce46319d9084d9cbf7cbabf99c2..8413bf93e1ca0ff07d019c5d1d5b80999711cc5b 100644
--- a/doc/mnist.rst
+++ b/doc/mnist.rst
@@ -68,7 +68,7 @@ The CAISAR standard library `caisar.mlw
 <https://git.frama-c.com/pub/caisar/-/blob/master/stdlib/caisar.mlw>`_ provides
 some utilities for dealing with verification problems about classification
 datasets. Of particular interest for us is the ``robust`` predicate, defined in
-the theory ``DataSetProps`` as follows:
+the theory ``DatasetClassificationProps`` as follows:
 
 .. code-block:: whyml
 
@@ -79,7 +79,7 @@ Note that the predicate is defined over a ``model``, a ``dataset`` and a
 floating-point value ``eps``. The latter determines the perturbation
 :math:`\epsilon`. The other two are custom WhyML types that respectively
 formalize the notions of classifier and dataset in CAISAR. These types are
-respectively defined in the ``Model`` and ``DataSetClassification`` theories.
+both defined in the ``DatasetClassification`` theory.
 
 Moreover, it is defined in terms of the predicate ``robust_at`` that formalizes
 the local robustness property:
@@ -104,7 +104,7 @@ values of types ``model`` and ``dataset``. For the former, CAISAR makes
 available the constant ``model`` upon interpreting the ``AsArray`` sub-theory
 that is built by the extension of the Why3 standard library for recognizing
 neural network ONNX and NNet formats. For the latter, the CAISAR standard
-library provides the constant ``dataset`` in ``DataSetClassification`` that will
+library provides the constant ``dataset`` in ``DatasetClassification`` that will
 be interpreted as the actual dataset the user needs to provide via the
 command-line interface when launching a CAISAR verification.
 
@@ -117,8 +117,8 @@ dataset, with each element's feature pertubed by :math:`1 \%`, looks like this:
    theory MNIST
      use MNIST_256_2.AsArray
      use ieee_float.Float64
-     use caisar.DataSetClassification
-     use caisar.DataSetProps
+     use caisar.DatasetClassification
+     use caisar.DatasetClassificationProps
 
      goal robustness:
       let normalized_dataset = min_max_scale true (0.0:t) (1.0:t) dataset in
@@ -126,7 +126,7 @@ dataset, with each element's feature pertubed by :math:`1 \%`, looks like this:
    end
 
 Note the presence of the ``min_max_scale`` function defined in
-``DataSetClassification`` for normalizing all feature values in :math:`[0,1]`.
+``DatasetClassification`` for normalizing all feature values in :math:`[0,1]`.
 Besides classic *Min-Max scaling*, CAISAR also provides ``z_norm`` function for
 *Z-normalization*.
 
diff --git a/examples/mnist/property.why b/examples/mnist/property.why
index 9f47a84b1a8f52b0c694a3e33f800eac10fc3a28..cef1ef733df08ab3110d954c656e3a0c76927517 100644
--- a/examples/mnist/property.why
+++ b/examples/mnist/property.why
@@ -1,8 +1,8 @@
 theory MNIST
   use MNIST_256_2.AsArray
   use ieee_float.Float64
-  use caisar.DataSetClassification
-  use caisar.DataSetProps
+  use caisar.DatasetClassification
+  use caisar.DatasetClassificationProps
 
   goal robustness:
    let normalized_dataset = min_max_scale true (0.0:t) (1.0:t) dataset in
diff --git a/src/dataset.ml b/src/dataset.ml
index 81544a9f8e33f19fd1c985bb310c2e329f5145a1..cf7586483aaf3955c5ad32bead31b61b797b6204 100644
--- a/src/dataset.ml
+++ b/src/dataset.ml
@@ -141,7 +141,7 @@ let interpret_normalization =
     []
 
 let term_of_normalization env normalization =
-  let th = Pmodule.read_module env [ "caisar" ] "DataSetClassification" in
+  let th = Pmodule.read_module env [ "caisar" ] "DatasetClassification" in
   let t_dataset =
     let ls_dataset = Theory.ns_find_ls th.mod_theory.th_export [ "dataset" ] in
     Term.t_app_infer ls_dataset []
@@ -193,7 +193,7 @@ let string_of_predicate_kind = function
   | CondRobust _ -> "condrobust"
 
 let find_predicate_ls env p =
-  let th = Pmodule.read_module env [ "caisar" ] "DataSetProps" in
+  let th = Pmodule.read_module env [ "caisar" ] "DatasetClassificationProps" in
   Theory.ns_find_ls th.mod_theory.th_export [ p ]
 
 let failwith_unsupported_term t =
diff --git a/src/language.ml b/src/language.ml
index 789d5bc6a2f101bd9e3267504dfd3b562424fa33..7d7abb4cdbef4f582390f7462b46418449c1c08e 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -72,7 +72,7 @@ let register_nn_as_tuple env nb_inputs nb_outputs filename ?nier mstr =
 let register_nn_as_array env nb_inputs nb_outputs filename ?nier mstr =
   let name = "AsArray" in
   let th_uc = Pmodule.create_module env (Ident.id_fresh name) in
-  let nn = Pmodule.read_module env [ "caisar" ] "Model" in
+  let nn = Pmodule.read_module env [ "caisar" ] "DatasetClassification" in
   let th_uc = Pmodule.use_export th_uc nn in
   let ty_data =
     Ty.ty_app Theory.(ns_find_ts nn.mod_theory.th_export [ "model" ]) []
@@ -89,7 +89,7 @@ let register_nn_as_array env nb_inputs nb_outputs filename ?nier mstr =
 let register_svm_as_array env nb_inputs nb_classes filename mstr =
   let name = "AsArray" in
   let th_uc = Pmodule.create_module env (Ident.id_fresh name) in
-  let svm = Pmodule.read_module env [ "caisar" ] "Model" in
+  let svm = Pmodule.read_module env [ "caisar" ] "DatasetClassification" in
   let th_uc = Pmodule.use_export th_uc svm in
   let svm_type =
     Ty.ty_app Theory.(ns_find_ts svm.mod_theory.th_export [ "model" ]) []
diff --git a/src/verification.ml b/src/verification.ml
index 0376258b67b0141ec78cbecd5a43e9f39df11f1a..2e5b2f9497af752c70a72badb93255630d016213 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -90,20 +90,19 @@ module JSON = struct
       (Wstdlib.Mstr.find "AsArray" pmod).mod_theory
     in
     let th_float64 = Env.read_theory env [ "ieee_float" ] "Float64" in
-    let th_ds_classification =
-      Pmodule.read_module env [ "caisar" ] "DataSetClassification"
+    let th_dsc = Pmodule.read_module env [ "caisar" ] "DatasetClassification" in
+    let th_dsc_props =
+      Pmodule.read_module env [ "caisar" ] "DatasetClassificationProps"
     in
-    let th_ds_props = Pmodule.read_module env [ "caisar" ] "DataSetProps" in
     let name = "JSON" in
     let th_uc = Theory.create_theory (Ident.id_fresh name) in
     let th_uc = Theory.use_export th_uc th_as_array in
     let th_uc = Theory.use_export th_uc th_float64 in
-    let th_uc = Theory.use_export th_uc th_ds_classification.mod_theory in
-    let th_uc = Theory.use_export th_uc th_ds_props.mod_theory in
+    let th_uc = Theory.use_export th_uc th_dsc.mod_theory in
+    let th_uc = Theory.use_export th_uc th_dsc_props.mod_theory in
     let t_dataset =
       let ls_dataset =
-        Theory.ns_find_ls th_ds_classification.mod_theory.th_export
-          [ "dataset" ]
+        Theory.ns_find_ls th_dsc.mod_theory.th_export [ "dataset" ]
       in
       Term.t_app_infer ls_dataset []
     in
@@ -120,8 +119,7 @@ module JSON = struct
         let ls_dataset_norm =
           let ty =
             Ty.ty_app
-              (Theory.ns_find_ts th_ds_classification.mod_theory.th_export
-                 [ "dataset" ])
+              (Theory.ns_find_ts th_dsc.mod_theory.th_export [ "dataset" ])
               []
           in
           Term.create_fsymbol (Ident.id_fresh "dataset'") [] ty
@@ -138,12 +136,12 @@ module JSON = struct
         match t.property.kind with
         | Dataset.Correct ->
           let ls_correct =
-            Theory.ns_find_ls th_ds_props.mod_theory.th_export [ "correct" ]
+            Theory.ns_find_ls th_dsc_props.mod_theory.th_export [ "correct" ]
           in
           Term.t_app_infer ls_correct [ t_model; t_dataset ]
         | Robust eps ->
           let ls_robust =
-            Theory.ns_find_ls th_ds_props.mod_theory.th_export [ "robust" ]
+            Theory.ns_find_ls th_dsc_props.mod_theory.th_export [ "robust" ]
           in
           let t_eps = Dataset.term_of_eps env eps in
           Term.t_app_infer ls_robust [ t_model; t_dataset; t_eps ]
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 889f92be052088c797fe12645f1582341b6ed76e..fd0eacf17c2c6837767a315e6c2c1d2ab21f0cf8 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -20,69 +20,54 @@
 (*                                                                        *)
 (**************************************************************************)
 
-theory DataSetClassification
+theory DatasetClassification
   use ieee_float.Float64
   use int.Int
   use array.Array
 
   type features = array t
   type label_ = int
-
-  type datum = (features, label_)
-
-  type dataset = {
-    nb_features: int;
-    nb_label_s: int;
-    data: array datum
-  }
+  type record = (features, label_)
+  type dataset = array record
 
   constant dataset: dataset
 
   function min_max_scale (clip: bool) (min: t) (max: t) (d: dataset): dataset
   function z_norm (mean: t) (std_dev: t) (d: dataset): dataset
-end
-
-theory Model
-  use int.Int
-  use DataSetClassification
 
-  type model = {
-    nb_inputs: int;
-    nb_outputs: int;
-  }
+  type model
 
   function predict: model -> features -> label_
 end
 
-theory DataSetProps
+theory DatasetClassificationProps
   use ieee_float.Float64
   use int.Int
   use array.Array
-  use Model
-  use DataSetClassification
+  use DatasetClassification
 
   predicate linfty_distance (a: features) (b: features) (eps: t) =
     a.length = b.length /\
     forall i: int. 0 <= i < a.length -> .- eps .< a[i] .- b[i] .< eps
 
-  predicate correct_at (m: model) (d: datum) =
+  predicate correct_at (m: model) (d: record) =
     let (x, y) = d in
-    y = predict m x
+    predict m x = y
 
-  predicate robust_at (m: model) (d: datum) (eps: t) =
+  predicate robust_at (m: model) (d: record) (eps: t) =
     forall x': features.
       let (x, _) = d in
       linfty_distance x x' eps ->
       predict m x = predict m x'
 
-  predicate cond_robust_at (m: model) (d: datum) (eps: t) =
+  predicate cond_robust_at (m: model) (d: record) (eps: t) =
     correct_at m d /\ robust_at m d eps
 
   predicate correct (m: model) (d: dataset) =
-    forall i: int. 0 <= i < d.data.length -> correct_at m d.data[i]
+    forall i: int. 0 <= i < d.length -> correct_at m d[i]
 
   predicate robust (m: model) (d: dataset) (eps: t) =
-    forall i: int. 0 <= i < d.data.length -> robust_at m d.data[i] eps
+    forall i: int. 0 <= i < d.length -> robust_at m d[i] eps
 
   predicate cond_robust (m: model) (d: dataset) (eps: t) =
     correct m d /\ robust m d eps
@@ -91,7 +76,6 @@ end
 theory NN
   (** Module defining commonly-met operations in neural networks. *)
   use ieee_float.Float64
-  use Model
 
   type input_type = t
 
diff --git a/tests/dataset.t b/tests/dataset.t
index 6f05063743d0de5e3bc175e7cf99e62f81b1da5d..4c14126dd05a4c451e1c826c3ee323367c9ab0f1 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -18,8 +18,8 @@ Test verify
   > theory T
   >   use TestNetwork.AsArray as TN
   >   use ieee_float.Float64
-  >   use caisar.DataSetClassification
-  >   use caisar.DataSetProps
+  >   use caisar.DatasetClassification
+  >   use caisar.DatasetClassificationProps
   > 
   >   goal G: correct TN.model dataset
   > 
@@ -35,8 +35,8 @@ Test verify
   > theory T
   >   use TestNetwork.AsArray as TN
   >   use ieee_float.Float64
-  >   use caisar.DataSetClassification
-  >   use caisar.DataSetProps
+  >   use caisar.DatasetClassification
+  >   use caisar.DatasetClassificationProps
   > 
   >   goal G: correct TN.model dataset
   > 
diff --git a/tests/saver.t b/tests/saver.t
index ea252a3128ecccb2549d089ba0370dda592bfd4e..56387c8ebdf9ac41f0bf45865f3295c16f63fad1 100644
--- a/tests/saver.t
+++ b/tests/saver.t
@@ -15,8 +15,8 @@ Test verify
   > theory T
   >   use TestSVM.AsArray
   >   use ieee_float.Float64
-  >   use caisar.DataSetClassification
-  >   use caisar.DataSetProps
+  >   use caisar.DatasetClassification
+  >   use caisar.DatasetClassificationProps
   > 
   >   goal G: robust model dataset (8.0:t)
   >   goal H: correct model dataset