# HG changeset patch
# User slotosch
# Date 861975111 -7200
# Node ID 9d6526cacc3c94888f720db72742a7ebc73c8b49
# Parent  a5a42ff18a40def1d487d84e95227f16cf23bd0e
changed Domain->Dom for SML/NJ

diff -r a5a42ff18a40 -r 9d6526cacc3c src/HOL/Quot/PER0.ML
--- a/src/HOL/Quot/PER0.ML	Fri Apr 25 15:24:07 1997 +0200
+++ b/src/HOL/Quot/PER0.ML	Fri Apr 25 15:31:51 1997 +0200
@@ -42,12 +42,12 @@
 be per_sym 1;
 qed "sym2refl2";
 
-val prems = goalw thy [Domain] "x:D ==> x === x";
+val prems = goalw thy [Dom] "x:D ==> x === x";
 by (cut_facts_tac prems 1);
 by (fast_tac set_cs 1);
 qed "DomainD";
 
-val prems = goalw thy [Domain] "x === x ==> x:D";
+val prems = goalw thy [Dom] "x === x ==> x:D";
 by (cut_facts_tac prems 1);
 by (fast_tac set_cs 1);
 qed "DomainI";
@@ -73,14 +73,14 @@
 be (sym2refl2 RS DomainI) 1;
 qed "DomainI_right"; 
 
-val prems = goalw thy [Domain] "x~:D ==> ~x===y";
+val prems = goalw thy [Dom] "x~:D ==> ~x===y";
 by (cut_facts_tac prems 1);
 by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);ba 1;
 bd sym2refl1 1;
 by (fast_tac set_cs 1);
 qed "notDomainE1"; 
 
-val prems = goalw thy [Domain] "x~:D ==> ~y===x";
+val prems = goalw thy [Dom] "x~:D ==> ~y===x";
 by (cut_facts_tac prems 1);
 by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);ba 1;
 bd sym2refl2 1;
diff -r a5a42ff18a40 -r 9d6526cacc3c src/HOL/Quot/PER0.thy
--- a/src/HOL/Quot/PER0.thy	Fri Apr 25 15:24:07 1997 +0200
+++ b/src/HOL/Quot/PER0.thy	Fri Apr 25 15:31:51 1997 +0200
@@ -16,8 +16,8 @@
 
 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"
-        ax_per_trans    "[|eqv x y; eqv y z|] ==> eqv x z"
 
 axclass er < per
 	ax_er_refl	"eqv x x"
@@ -27,7 +27,7 @@
         D         :: "'a::per set"
 defs
         per_def         "(op ===) == eqv"
-        Domain          "D=={x.x===x}"
+        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"