7 *)
8
9 use_thy "Reflection";
10 use_thy "WF_absolute";
11 use_thy "L_axioms";
12 use_thy "Datatype_absolute";