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