src/HOL/Finite_Set.ML
changeset 17274 746bb4c56800
parent 16733 236dfafbeb63
child 21019 650c48711c7b
     1.1 --- a/src/HOL/Finite_Set.ML	Tue Sep 06 16:29:39 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.ML	Tue Sep 06 16:59:48 2005 +0200
     1.3 @@ -51,7 +51,6 @@
     1.4  val empty_foldSetE = thm "empty_foldSetE";
     1.5  val endo_inj_surj = thm "endo_inj_surj";
     1.6  val finite = thm "finite";
     1.7 -val finiteI = thm "finiteI";
     1.8  val finite_Diff = thm "finite_Diff";
     1.9  val finite_Diff_insert = thm "finite_Diff_insert";
    1.10  val finite_Field = thm "finite_Field";