1open HolKernel Parse boolLib 2 3val _ = new_theory "github115a" 4 5val v1 = mk_var("v", bool --> bool) 6val v2 = mk_var("v", bool) 7 8val t = mk_forall(v1, v2) 9 10val atoms = all_atoms t 11 12val _ = assert 13 (fn _ => length (HOLset.listItems atoms) = 3 andalso 14 HOLset.member(atoms, v1) andalso 15 HOLset.member(atoms, v2)) 16 t 17 18val th = save_thm("th", DISCH_ALL (ASSUME t)) 19 20val _ = export_theory() 21