Never used and not relevant.

--- 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";

--- a/src/HOL/Quot/FRACT.thy	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title:      HOL/Quot/FRACT.thy
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
-
-Example for higher order quotients: fractions
-*)
-
-FRACT = NPAIR + HQUOT +
-instance 
-	NP::per	
-	{| (etac per_trans_NP 1) THEN (atac 1) THEN (etac per_sym_NP 1) |}
-
-(* now define fractions *)
-
-types fract = NP quot
-
-(* example for fractions *)
-consts 
-	half ::	"fract"
-
-defs    half_def    "half == <[abs_NP(1,2)]>"
-end

--- a/src/HOL/Quot/HQUOT.ML	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,156 +0,0 @@
-(*  Title:      HOL/Quot/HQUOT.ML
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
-
-*)
-
-(* first prove some helpful lemmas *)
-Goalw [quot_def] "{y. y===x}:quot";
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [per_sym]) 1);
-qed "per_class_rep_quot";
-
-Goal "Rep_quot a = Rep_quot b ==> a=b";
-by (rtac (Rep_quot_inverse RS subst) 1);
-by (res_inst_tac [("t","a")] (Rep_quot_inverse RS subst) 1);
-by (Asm_simp_tac 1);
-qed "quot_eq";
-
-(* prepare induction and exhaustiveness *)
-Goal "!s. s:quot --> P (Abs_quot s) ==> P x";
-by (rtac (Abs_quot_inverse RS subst) 1);
-by (rtac Rep_quot 1);
-by (dres_inst_tac [("x","Rep_quot x")] spec 1);
-by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
-qed "all_q";
-
-Goal "? s. s:quot & x=Abs_quot s";
-by (res_inst_tac [("x","Rep_quot x")] exI 1);
-by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
-qed "exh_q";
-
-(* some lemmas for the equivalence classes *)
-
-(* equality and symmetry for equivalence classes *)
-Goalw [peclass_def] "x===y==><[x]>=<[y]>";
-by (res_inst_tac [("f","Abs_quot")] arg_cong 1);
-by (rtac Collect_cong 1);
-by (rtac iffI 1);
-by (etac per_trans 1);by (assume_tac 1);
-by (etac per_trans 1);
-by (etac per_sym 1);
-qed "per_class_eqI";
-
-Goalw [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y";
-by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
-by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
-by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
-by Safe_tac;
-by (blast_tac (claset() addIs [er_refl]) 1);
-qed "er_class_eqE";
-
-Goalw [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y";
-by (dtac DomainD 1);
-by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
-by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
-by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
-by Auto_tac;
-qed "per_class_eqE";
-
-Goal "<[(x::'a::er)]>=<[y]>=x===y";
-by (rtac iffI 1);
-by (etac er_class_eqE 1);
-by (etac per_class_eqI 1);
-qed "er_class_eq";
-
-Goal "x:D==><[x]>=<[y]>=x===y";
-by (rtac iffI 1);
-by (etac per_class_eqE 1);by (assume_tac 1);
-by (etac per_class_eqI 1);
-qed "per_class_eq";
-
-(* inequality *)
-Goal "[|x:D;~x===y|]==><[x]>~=<[y]>";
-by (rtac notI 1);
-by (dtac per_class_eqE 1);
-by Auto_tac;
-qed "per_class_neqI";
-
-Goal "~(x::'a::er)===y==><[x]>~=<[y]>";
-by (rtac notI 1);
-by (dtac er_class_eqE 1);
-by Auto_tac;
-qed "er_class_neqI";
-
-Goal "<[x]>~=<[y]>==>~x===y";
-by (rtac notI 1);
-by (etac notE 1);
-by (etac per_class_eqI 1);
-qed "per_class_neqE";
-
-Goal "x:D==><[x]>~=<[y]>=(~x===y)";
-by (rtac iffI 1);
-by (etac per_class_neqE 1);
-by (etac per_class_neqI 1);by (assume_tac 1);
-qed "per_class_not";
-
-Goal "<[(x::'a::er)]>~=<[y]>=(~x===y)";
-by (rtac iffI 1);
-by (etac per_class_neqE 1);
-by (etac er_class_neqI 1);
-qed "er_class_not";
-
-(* exhaustiveness and induction *)
-Goalw [peclass_def] "? s. x=<[s]>";
-by (rtac all_q 1);
-by (strip_tac 1);
-by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
-by (etac exE 1);
-by (res_inst_tac [("x","r")] exI 1);
-by (rtac quot_eq 1);
-by (subgoal_tac "s:quot" 1);
-by (asm_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
-by (rtac set_ext 1);
-by (Blast_tac 1);
-by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
-by (Blast_tac 1);
-qed "per_class_exh";
-
-Goal "!x. P<[x]> ==> P s";
-by (cut_facts_tac [read_instantiate[("x","s::'a::per quot")] per_class_exh] 1);
-by (Blast_tac 1);
-qed "per_class_all";
-
-(* theorems for any_in *)
-Goalw [any_in_def,peclass_def] "any_in<[(s::'a::er)]>===s";
-by (rtac selectI2 1);
-by (rtac refl 1);
-by (fold_goals_tac [peclass_def]);
-by (etac er_class_eqE 1);
-qed "er_any_in_class";
-
-Goalw [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
-by (rtac selectI2 1);
-by (rtac refl 1);
-by (fold_goals_tac [peclass_def]);
-by (rtac per_sym 1);
-by (etac per_class_eqE 1);
-by (etac sym 1);
-qed "per_any_in_class";
-
-Goal "<[any_in (s::'a::er quot)]> = s";
-by (rtac per_class_all 1);
-by (rtac allI 1);
-by (rtac (er_any_in_class RS per_class_eqI) 1);
-qed "er_class_any_in";
-
-(* equivalent theorem for per would need !x.x:D *)
-Goal "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
-by (rtac per_class_all 1);
-by (rtac allI 1);
-by (rtac (per_any_in_class RS per_class_eqI) 1);
-by (etac spec 1);
-qed "per_class_any_in";
-
-(* is like theorem for class er *)

--- a/src/HOL/Quot/HQUOT.thy	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      HOL/Quot/HQUOT.thy
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
-
-quotient constructor for higher order quotients
-
-*)
-
-HQUOT = PER +      
-
-typedef 'a quot = "{s::'a::per set. ? r.!y. y:s=y===r}" (quotNE)
-
-(* constants for equivalence classes *)
-consts
-        peclass         :: "'a::per => 'a quot"
-        any_in          :: "'a::per quot => 'a"
-
-syntax          "@ecl"  :: "'a::per => 'a quot" ("<[ _ ]>")
-
-translations    "<[x]>" == "peclass x"
-
-defs
-        peclass_def     "<[x]> == Abs_quot {y. y===x}"
-        any_in_def      "any_in f == @x.<[x]>=f"
-end
-

--- a/src/HOL/Quot/NPAIR.ML	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      HOL/Quot/NPAIR.ML
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
-
-*)
-open NPAIR;
-
-Goalw [rep_NP_def] "rep_NP(abs_NP np) = np";
-by Auto_tac;
-qed "rep_abs_NP";
-
-Addsimps [rep_abs_NP];
-
-Goalw [per_NP_def] "eqv (x::NP) y ==> eqv y x";
-by Auto_tac;
-qed "per_sym_NP";
-

--- a/src/HOL/Quot/NPAIR.thy	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title:      HOL/Quot/NPAIR.thy
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
-
-Example: define a PER on pairs of natural numbers (with embedding)
-
-*)
-NPAIR = PER + Main + (* representation for rational numbers *)
-
-datatype NP = abs_NP "(nat * nat)"
-
-consts	rep_NP :: "NP => nat * nat"
-
-defs    rep_NP_def "rep_NP x == (case x of abs_NP y => y)"
-
-(* NPAIR (continued) *)
-defs	per_NP_def 
-  "eqv ==(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
-
-(* for proves of this rule see [Slo97diss] *)
-rules
-	per_trans_NP	"[| eqv (x::NP) y;eqv y z |] ==> eqv x z"
-end

--- a/src/HOL/Quot/PER.ML	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      HOL/Quot/PER.ML
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
-
-*)
-open PER;
-
-Goalw [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)";
-by (rtac refl 1);
-qed "inst_fun_per";
-
-(* Witness that quot is not empty *)
-Goal "?z:{s.? r.!y. y:s=y===r}";
-by (rtac CollectI 1);
-by (res_inst_tac [("x","x")] exI 1);
-by (rtac allI 1);
-by (rtac mem_Collect_eq 1);
-qed "quotNE";

--- a/src/HOL/Quot/PER.thy	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(*  Title:      HOL/Quot/PER.thy
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
-
-instances for per - makes PER higher order
-*)
-
-PER = PER0 + (* instance for per *)
-
-instance fun  :: (per,per)per   
-{| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |}
-
-end

--- a/src/HOL/Quot/PER0.ML	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,103 +0,0 @@
-(*  Title:      HOL/Quot/PER0.ML
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
-
-*)
-open PER0;
-
-(* derive the characteristic axioms *)
-Goalw [per_def] "x === y ==> y === x";
-by (etac ax_per_sym 1);
-qed "per_sym";
-
-Goalw [per_def] "[| x === y; y === z |] ==> x === z";
-by (etac ax_per_trans 1);
-by (assume_tac 1);
-qed "per_trans";
-
-Goalw [per_def] "(x::'a::er) === x";
-by (rtac ax_er_refl 1);
-qed "er_refl";
-
-(* now everything works without axclasses *)
-
-Goal "x===y=y===x";
-by (rtac iffI 1);
-by (etac per_sym 1);
-by (etac per_sym 1);
-qed "per_sym2";
-
-Goal "x===y ==> x===x";
-by (rtac per_trans 1);by (assume_tac 1);
-by (etac per_sym 1);
-qed "sym2refl1";
-
-Goal "x===y ==> y===y";
-by (rtac per_trans 1);by (assume_tac 2);
-by (etac per_sym 1);
-qed "sym2refl2";
-
-Goalw [Dom] "x:D ==> x === x";
-by (Blast_tac 1);
-qed "DomainD";
-
-Goalw [Dom] "x === x ==> x:D";
-by (Blast_tac 1);
-qed "DomainI";
-
-Goal "x:D = x===x";
-by (rtac iffI 1);
-by (etac DomainD 1);
-by (etac DomainI 1);
-qed "DomainEq";
-
-Goal "(~ x === y) = (~ y === x)";
-by (rtac (per_sym2 RS arg_cong) 1);
-qed "per_not_sym";
-
-(* show that PER work only on D *)
-Goal "x===y ==> x:D";
-by (etac (sym2refl1 RS DomainI) 1);
-qed "DomainI_left"; 
-
-Goal "x===y ==> y:D";
-by (etac (sym2refl2 RS DomainI) 1);
-qed "DomainI_right"; 
-
-Goalw [Dom] "x~:D ==> ~x===y";
-by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);
-by (assume_tac 1);
-by (dtac sym2refl1 1);
-by (Blast_tac 1);
-qed "notDomainE1"; 
-
-Goalw [Dom] "x~:D ==> ~y===x";
-by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);
-by (assume_tac 1);
-by (dtac sym2refl2 1);
-by (Blast_tac 1);
-qed "notDomainE2"; 
-
-(* theorems for equivalence relations *)
-Goal "(x::'a::er) : D";
-by (rtac DomainI 1);
-by (rtac er_refl 1);
-qed "er_Domain";
-
-(* witnesses for "=>" ::(per,per)per  *)
-Goalw [fun_per_def]"eqv (x::'a::per => 'b::per) y ==> eqv y x";
-by (auto_tac (claset(), simpset() addsimps [per_sym2]));
-qed "per_sym_fun";
-
-Goalw [fun_per_def] "[| eqv (f::'a::per=>'b::per) g;eqv g h|] ==> eqv f h";
-by Safe_tac;
-by (REPEAT (dtac spec 1));
-by (res_inst_tac [("y","g y")] per_trans 1);
-by (rtac mp 1);by (assume_tac 1);
-by (Asm_simp_tac 1);
-by (rtac mp 1);by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [sym2refl2]) 1);
-qed "per_trans_fun";
-
-

--- a/src/HOL/Quot/PER0.thy	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(*  Title:      HOL/Quot/PER0.thy
-    ID:         $Id$
-    Author:     Oscar Slotosch
-    Copyright   1997 Technische Universitaet Muenchen
-
-Definition of classes per and er for (partial) equivalence classes
-The polymorphic constant eqv is only for the definition of PERs
-The characteristic constant === (sim) is available on the class per
-
-*)
-
-PER0 = Set + (* partial equivalence relations *)
-
-consts  (* polymorphic constant for (partial) equivalence relations *)
-        eqv    :: "'a::term => 'a => bool" 
-
-axclass per < term
-	(* axioms for partial equivalence relations *)
-        ax_per_trans    "[|eqv x y; eqv y z|] ==> eqv x z"
-        ax_per_sym      "eqv x y ==> eqv y x"
-
-axclass er < per
-	ax_er_refl	"eqv x x"
-
-consts  (* characteristic constant and Domain for per *)
-        "==="     :: "'a::per => 'a => bool" (infixl 55)
-        D         :: "'a::per set"
-defs
-        per_def         "(op ===) == eqv"
-        Dom             "D=={x. x===x}"
-(* define ==== on and function type => *)
-        fun_per_def     "eqv f g == !x y. x:D & y:D & x===y --> f x === g y"
-
-syntax (symbols)
-  "op ==="   :: "['a,'a::per] => bool"        (infixl "\\<sim>" 50)
-
-end

--- a/src/HOL/Quot/README	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-This directorty contains the higher order quotients in Isabelle HOL
-
-higher order quotients use partial equivalence relations/classes (PERs) 
-instead of euivalence relations/classes
-We have two classes er<per
-
-Quotients are a specialization of higher order quotients.
-The use the same constructor quot with the subclass er.
-
-An Example for the application of quotients are the fractions.
-The example shows how to define an equivalence relation and how to use
-the quotients.
-
-For a more detailed description see [Slo97].

--- a/src/HOL/Quot/ROOT.ML	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      HOL/Quot/ROOT.ML
-    ID:         $Id$
-
-Higher-order quotients.
-*)
-
-time_use_thy "FRACT";