--- a/src/HOLCF/Holcfb.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/Holcfb.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -13,32 +13,5 @@
 (* ------------------------------------------------------------------------ *)
 
 
-(* val de_morgan1 = de_Morgan_disj RS sym;   "(~a & ~b)=(~(a | b))" *)
-
-(* val de_morgan2 = de_Morgan_conj RS sym;   "(~a | ~b)=(~(a & b))" *)
-
-
-(* val notall2ex = not_all                   "(~ (!x.P(x))) = (? x.~P(x))" *)
-
-(* val notex2all = not_ex                    "(~ (? x.P(x))) = (!x.~P(x))" *)
-
-
-(* val selectI3 =  select_eq_Ex RS iffD2   "(? x. P(x)) ==> P(@ x.P(x))" *)
-
-(* val selectE =   select_eq_Ex RS iffD1   "P(@ x.P(x)) ==> (? x. P(x))" *)
-
-
-(*
-qed_goal "notnotI" HOL.thy "P ==> ~~P"
-(fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (fast_tac HOL_cs 1)
-        ]);
-*)
-
-(* val classical2 = case_split_thm;        "[|Q ==> R; ~Q ==> R|]==>R" *)
-
-(* fun case_tac s = res_inst_tac [("Q",s)] classical2; *)
 
 val classical3 = (notE RS notI); (* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)