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