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