1open HolKernel Parse boolLib
2open addMLdep1Theory
3
4val _ = new_theory "addMLdep2";
5
6fun grep s fname =
7  let
8    val instr = TextIO.openIn fname
9    fun recurse () =
10      case TextIO.inputLine instr of
11          NONE => false
12        | SOME line => String.isSubstring s line orelse recurse ()
13  in
14    recurse() before TextIO.closeIn instr
15  end
16
17val _ = if grep "MLdepLib" "addMLdep1Theory.sml" then ()
18        else OS.Process.exit OS.Process.failure
19
20val _ = save_thm("thm2", TRUTH);
21
22val _ = export_theory();
23