session Span in src = HOL + options [document = false] sessions "HOL-Library" directories "../tests" theories Model Layout Relax Encoding Machine Frontend Examples Export