5 in use pattern "cic:/Coq/Reals/Rdefinitions/Rlt.con" position $s0
6 where $s0 is mainconclusion
11 open Mathql_semantics;;
14 (* stampa tutti i documenti che fanno match con un pattern di input *)
16 (function atturi -> print_endline ("output: " ^ atturi))
27 [MQBD; MQBC"Algebra"; MQBD; MQBC "Basics"; MQBD; MQBSS],