xref: /seL4-l4v-master/HOL4/src/1/theory_tests/gh225aScript.sml

open HolKernel Parse boolLib

val _ = new_theory "gh225a";

val _ = save_thm("Empty", TRUTH);
val _ = save_thm("GREATER", TRUTH);


val _ = export_theory();