1open HolKernel Parse boolLib bossLib;
2
3val _ = new_theory "comp_delbinding1";
4
5(* compset now has foo_def in it *)
6val foo_def = Define���foo x = x + 1���;
7
8val _ = case ThmSetData.current_data{settype="compute"} of
9            [ThmSetData.ADD({Thy = "comp_delbinding1", Name = "foo_def"}, _)] =>
10              print "Compute data OK\n"
11          | _ => raise Fail "Compute data Bad!"
12
13val _ =
14    case LoadableThyData.segment_data
15           {thy="comp_delbinding1", thydataty="compute"}
16     of
17        NONE => raise Fail "No compute data for LTD.segment_data"
18      | SOME t => print "LTD.segment_data exists\n"
19
20(* now replace "foo_def" binding with something else; the old binding
21   should drop out of the compset
22*)
23Theorem foo_def = REFL ``x:num``
24
25val _ = null (ThmSetData.current_data{settype="compute"}) orelse
26        raise Fail "compute data not empty!"
27
28val th = EVAL ���foo 2���
29val _ = rhs (concl th) ~~ lhs (concl th) orelse
30        (print "foo was evaluated - unfortunate but unavoidable perhaps!\n";
31         true)
32
33
34
35val _ = export_theory();
36