src/HOL/SPARK/Manual/ROOT.ML

using the new transfer method to obtain abstract properties of RBT trees

Printer.show_question_marks_default := false;

use_thys
  ["Example_Verification",
   "VC_Principles",
   "Reference",
   "Complex_Types"];