1open HolKernel Parse boolLib Datatype 2 3val _ = new_theory "gh224a"; 4 5(* val _ = Datatype `bar = <| size : num |>` *) 6 7val _ = Datatype `A_x = <| y : num |>` 8val _ = Datatype `A = <| x : A_x |>` 9 10 11val _ = export_theory(); 12