--- a/src/HOL/BCV/Types.ML Fri Sep 01 18:01:05 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* Title: HOL/BCV/Types.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1999 TUM
-*)
-
-Goalw [semilat_def,le_typ,plus_typ] "semilat (UNIV::typ set)";
-by (Auto_tac);
-qed "semilat_typ";
-AddIffs [semilat_typ];
-
-Goal "{(x,y::'a::order). y<x}^+ = {(x,y::'a::order). y<x}";
-by (Auto_tac);
- by (etac trancl_induct 1);
- by (Blast_tac 1);
- by (blast_tac (claset() addIs [order_less_trans]) 1);
-by (blast_tac (claset() addIs [r_into_trancl]) 1);
-qed "trancl_order1_conv";
-Addsimps [trancl_order1_conv];
-
-Goalw [acyclic_def] "acyclic{(x,y::'a::order). y<x}";
-by (Simp_tac 1);
-qed "acyclic_order1";
-AddIffs [acyclic_order1];
-
-Goalw [acc_def] "acc(UNIV::typ set)";
-by (rtac finite_acyclic_wf 1);
- by (fast_tac (claset() addIs [finite_SigmaI RSN (2,finite_subset)]) 1);
-by (blast_tac (claset() addIs [acyclic_subset]) 1);
-qed "acc_UNIV_typ";
-AddIffs [acc_UNIV_typ];