xref: /seL4-l4v-10.1.1/HOL4/src/1/theory_tests/readthm1Script.sml

open HolKernel Parse boolLib

val _ = new_theory "readthm1";

val read = save_thm("read", TRUTH);


val _ = export_theory();