1open HolKernel Parse boolLib 2 3open monofldATheory 4 5val _ = new_theory "monofldB"; 6 7val (write, read) = let 8 val buf = ref ([] : string list) 9 fun w s = (buf := s :: !buf) 10 fun r () = let 11 val result = String.concat (List.rev (!buf)) 12 in 13 buf := [result]; 14 result 15 end 16in 17 (w, r) 18end 19 20val _ = Feedback.MESG_outstream := write 21val _ = Globals.interactive := true 22 23val t = ``(r : 'a rcd) with myset := (\x. F)``; 24 25val _ = assert (equal ``:'a rcd``) (type_of t) 26 27val msg = read() 28val _ = if msg = "" then print "No message\n" 29 else raise Fail ("Message was: "^msg) 30 31val _ = save_thm("MFB", TRUTH) 32 33val _ = export_theory(); 34