--- a/src/HOLCF/Void.ML Sat Feb 15 18:24:05 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* Title: HOLCF/void.ML
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for void.thy.
-
-These lemmas are prototype lemmas for class porder
-see class theory porder.thy
-*)
-
-open Void;
-
-(* ------------------------------------------------------------------------ *)
-(* A non-emptyness result for Void *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "VoidI" Void.thy [UU_void_Rep_def,Void_def]
- " UU_void_Rep : Void"
-(fn prems =>
- [
- (stac mem_Collect_eq 1),
- (rtac refl 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* less_void is a partial ordering on void *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "refl_less_void" Void.thy [ less_void_def ] "less_void x x"
-(fn prems =>
- [
- (fast_tac HOL_cs 1)
- ]);
-
-qed_goalw "antisym_less_void" Void.thy [ less_void_def ]
- "[|less_void x y; less_void y x|] ==> x = y"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac (Rep_Void_inverse RS subst) 1),
- (etac subst 1),
- (rtac (Rep_Void_inverse RS sym) 1)
- ]);
-
-qed_goalw "trans_less_void" Void.thy [ less_void_def ]
- "[|less_void x y; less_void y z|] ==> less_void x z"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (fast_tac HOL_cs 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* a technical lemma about void: *)
-(* every element in void is represented by UU_void_Rep *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "unique_void" Void.thy "Rep_Void(x) = UU_void_Rep"
-(fn prems =>
- [
- (rtac (mem_Collect_eq RS subst) 1),
- (fold_goals_tac [Void_def]),
- (rtac Rep_Void 1)
- ]);
-
-
-
-