--- a/src/HOL/Quot/FRACT.ML Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* Title: HOL/Quot/FRACT.ML
- ID: $Id$
- Author: Oscar Slotosch
- Copyright 1997 Technische Universitaet Muenchen
-
-*)
-
-Goalw [per_def,per_NP_def]
-"(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
-by (rtac refl 1);
-qed "inst_NP_per";
-
-
-Goalw [half_def] "half = <[abs_NP(n,#2*n)]>";
-by (rtac per_class_eqI 1);
-by (simp_tac (simpset() addsimps [inst_NP_per]) 1);
-qed "test";