1open HolKernel Parse boolLib
2
3val _ = new_theory "addDB";
4
5val foo_def = new_definition("foo_def", ���foo x <=> ~x���);
6
7val th1 = DB.fetch "-" "foo_def"
8val th2 = DB.fetch "addDB" "foo_def"
9
10Theorem foo_thm = CONJ TRUTH TRUTH
11
12val th3 = DB.fetch "-" "foo_thm"
13val th4 = DB.fetch "addDB" "foo_thm"
14val th5 = DB.fetch "-" "foo_def"
15
16Theorem foo_thm = CONJ TRUTH (REFL ���t:bool���)
17
18val th6 = DB.fetch "-" "foo_thm"
19
20val _ = length (DB.find "foo_") = 2 orelse raise Fail "bad DB.find"
21
22val _ = length (DB.definitions "-") = 1 orelse raise Fail "bad DB.definitions"
23val _ = length (DB.definitions "addDB") = 1 orelse
24        raise Fail "bad DB.definitions"
25val _ = length (DB.theorems "-") = 1 orelse raise Fail "bad DB.theorems"
26val _ = length (DB.theorems "addDB") = 1 orelse raise Fail "bad DB.theorems"
27
28val bar_def = new_definition("bar_def", ���bar x <=> x /\ foo x���);
29
30val _ = delete_const "bar"
31
32val _ = length (DB.definitions "-") = 1 orelse raise Fail "bad DB.definitions"
33
34
35val _ = export_theory();
36