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