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