# HG changeset patch
# User paulson
# Date 910960913 -3600
# Node ID beddc19c107a935904e75715d2d22981ab984e89
# Parent  701498a38a7623281008552b2fa9a9f78eb5e70a
needed tidying desperately

diff -r 701498a38a76 -r beddc19c107a src/HOL/Quot/FRACT.ML
--- a/src/HOL/Quot/FRACT.ML	Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/FRACT.ML	Fri Nov 13 13:41:53 1998 +0100
@@ -4,15 +4,14 @@
     Copyright   1997 Technische Universitaet Muenchen
 
 *)
-open FRACT;
 
 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))";
-fr refl;
+br refl 1;
 qed "inst_NP_per";
 
 
 Goalw [half_def] "half = <[abs_NP(n,2*n)]>";
-fr per_class_eqI;
+br per_class_eqI 1;
 by (simp_tac (simpset() addsimps [inst_NP_per]) 1);
 qed "test";
diff -r 701498a38a76 -r beddc19c107a src/HOL/Quot/HQUOT.ML
--- a/src/HOL/Quot/HQUOT.ML	Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/HQUOT.ML	Fri Nov 13 13:41:53 1998 +0100
@@ -4,24 +4,21 @@
     Copyright   1997 Technische Universitaet Muenchen
 
 *)
-open HQUOT;
 
 (* first prove some helpful lemmas *)
 Goalw [quot_def] "{y. y===x}:quot";
 by (Asm_simp_tac 1);
-by (fast_tac (set_cs addIs [per_sym]) 1);
+by (blast_tac (claset() addIs [per_sym]) 1);
 qed "per_class_rep_quot";
 
-val prems = goal thy "Rep_quot a = Rep_quot b ==> a=b";
-by (cut_facts_tac prems 1);
+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 *)
-val prems = goal thy "!s. s:quot --> P (Abs_quot s) ==> P x";
-by (cut_facts_tac prems 1);
+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);
@@ -36,8 +33,7 @@
 (* some lemmas for the equivalence classes *)
 
 (* equality and symmetry for equivalence classes *)
-val prems = goalw thy [peclass_def] "x===y==><[x]>=<[y]>";
-by (cut_facts_tac prems 1);
+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);
@@ -46,22 +42,20 @@
 by (etac per_sym 1);
 qed "per_class_eqI";
 
-val prems = goalw thy [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y";
-by (cut_facts_tac prems 1);
+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 set_cs);
-by (fast_tac (set_cs addIs [er_refl]) 1);
+by Safe_tac;
+by (blast_tac (claset() addIs [er_refl]) 1);
 qed "er_class_eqE";
 
-val prems = goalw thy [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y";
-by (cut_facts_tac prems 1);
+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 (safe_tac set_cs);
+by Auto_tac;
 qed "per_class_eqE";
 
 Goal "<[(x::'a::er)]>=<[y]>=x===y";
@@ -70,37 +64,32 @@
 by (etac per_class_eqI 1);
 qed "er_class_eq";
 
-val prems = goal thy "x:D==><[x]>=<[y]>=x===y";
-by (cut_facts_tac prems 1);
+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 *)
-val prems = goal thy "[|x:D;~x===y|]==><[x]>~=<[y]>";
-by (cut_facts_tac prems 1);
+Goal "[|x:D;~x===y|]==><[x]>~=<[y]>";
 by (rtac notI 1);
 by (dtac per_class_eqE 1);
 by Auto_tac;
 qed "per_class_neqI";
 
-val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>";
-by (cut_facts_tac prems 1);
+Goal "~(x::'a::er)===y==><[x]>~=<[y]>";
 by (rtac notI 1);
 by (dtac er_class_eqE 1);
 by Auto_tac;
 qed "er_class_neqI";
 
-val prems = goal thy "<[x]>~=<[y]>==>~x===y";
-by (cut_facts_tac prems 1);
+Goal "<[x]>~=<[y]>==>~x===y";
 by (rtac notI 1);
 by (etac notE 1);
 by (etac per_class_eqI 1);
 qed "per_class_neqE";
 
-val prems = goal thy "x:D==><[x]>~=<[y]>=(~x===y)";
-by (cut_facts_tac prems 1);
+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);
@@ -123,49 +112,45 @@
 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 (fast_tac set_cs 1);
+by (Blast_tac 1);
 by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
-by (fast_tac set_cs 1);
+by (Blast_tac 1);
 qed "per_class_exh";
 
-val prems = goal thy "!x. P<[x]> ==> P s";
-by (cut_facts_tac (prems@[
-	read_instantiate[("x","s::'a::per quot")] per_class_exh]) 1);
-by (fast_tac set_cs 1);
+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";
-fr selectI2;
-fr refl;
+br selectI2 1;
+br refl 1;
 by (fold_goals_tac [peclass_def]);
-fe er_class_eqE;
+be er_class_eqE 1;
 qed "er_any_in_class";
 
-val prems = goalw thy [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
-by (cut_facts_tac prems 1);
-fr selectI2;
-fr refl;
+Goalw [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
+br selectI2 1;
+br refl 1;
 by (fold_goals_tac [peclass_def]);
-fr per_sym;
-fe per_class_eqE;
-fe sym;
+br per_sym 1;
+be per_class_eqE 1;
+be sym 1;
 qed "per_any_in_class";
 
-val prems = goal thy "<[any_in (s::'a::er quot)]> = s";
-by (cut_facts_tac prems 1);
-fr per_class_all;
-fr allI;
-fr (er_any_in_class RS per_class_eqI);
+Goal "<[any_in (s::'a::er quot)]> = s";
+br per_class_all 1;
+br allI 1;
+br (er_any_in_class RS per_class_eqI) 1;
 qed "er_class_any_in";
 
 (* equivalent theorem for per would need !x.x:D *)
-val prems = goal thy "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
-by (cut_facts_tac prems 1);
-fr per_class_all;
-fr allI;
-fr (per_any_in_class RS per_class_eqI);
-fe spec;
+Goal "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
+br per_class_all 1;
+br allI 1;
+br (per_any_in_class RS per_class_eqI) 1;
+be spec 1;
 qed "per_class_any_in";
 
-(* is like theorem for class er *)
\ No newline at end of file
+(* is like theorem for class er *)
diff -r 701498a38a76 -r beddc19c107a src/HOL/Quot/NPAIR.ML
--- a/src/HOL/Quot/NPAIR.ML	Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/NPAIR.ML	Fri Nov 13 13:41:53 1998 +0100
@@ -12,8 +12,7 @@
 
 Addsimps [rep_abs_NP];
 
-val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
-by (cut_facts_tac prems 1);
+Goalw [per_NP_def] "eqv (x::NP) y ==> eqv y x";
 by Auto_tac;
 qed "per_sym_NP";
 
diff -r 701498a38a76 -r beddc19c107a src/HOL/Quot/PER.ML
--- a/src/HOL/Quot/PER.ML	Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/PER.ML	Fri Nov 13 13:41:53 1998 +0100
@@ -12,7 +12,7 @@
 
 (* Witness that quot is not empty *)
 Goal "?z:{s.? r.!y. y:s=y===r}";
-fr CollectI;
+br CollectI 1;
 by (res_inst_tac [("x","x")] exI 1);
 by (rtac allI 1);
 by (rtac mem_Collect_eq 1);
diff -r 701498a38a76 -r beddc19c107a src/HOL/Quot/PER0.ML
--- a/src/HOL/Quot/PER0.ML	Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/PER0.ML	Fri Nov 13 13:41:53 1998 +0100
@@ -7,13 +7,11 @@
 open PER0;
 
 (* derive the characteristic axioms *)
-val prems = goalw thy [per_def] "x === y ==> y === x";
-by (cut_facts_tac prems 1);
+Goalw [per_def] "x === y ==> y === x";
 by (etac ax_per_sym 1);
 qed "per_sym";
 
-val prems = goalw thy [per_def] "[| x === y; y === z |] ==> x === z";
-by (cut_facts_tac prems 1);
+Goalw [per_def] "[| x === y; y === z |] ==> x === z";
 by (etac ax_per_trans 1);
 by (assume_tac 1);
 qed "per_trans";
@@ -30,26 +28,22 @@
 by (etac per_sym 1);
 qed "per_sym2";
 
-val prems = goal  thy "x===y ==> x===x";
-by (cut_facts_tac prems 1);
+Goal "x===y ==> x===x";
 by (rtac per_trans 1);by (assume_tac 1);
 by (etac per_sym 1);
 qed "sym2refl1";
 
-val prems = goal  thy "x===y ==> y===y";
-by (cut_facts_tac prems 1);
+Goal "x===y ==> y===y";
 by (rtac per_trans 1);by (assume_tac 2);
 by (etac per_sym 1);
 qed "sym2refl2";
 
-val prems = goalw thy [Dom] "x:D ==> x === x";
-by (cut_facts_tac prems 1);
-by (fast_tac set_cs 1);
+Goalw [Dom] "x:D ==> x === x";
+by (Blast_tac 1);
 qed "DomainD";
 
-val prems = goalw thy [Dom] "x === x ==> x:D";
-by (cut_facts_tac prems 1);
-by (fast_tac set_cs 1);
+Goalw [Dom] "x === x ==> x:D";
+by (Blast_tac 1);
 qed "DomainI";
 
 Goal "x:D = x===x";
@@ -63,28 +57,26 @@
 qed "per_not_sym";
 
 (* show that PER work only on D *)
-val prems = goal thy "x===y ==> x:D";
-by (cut_facts_tac prems 1);
+Goal "x===y ==> x:D";
 by (etac (sym2refl1 RS DomainI) 1);
 qed "DomainI_left"; 
 
-val prems = goal thy "x===y ==> y:D";
-by (cut_facts_tac prems 1);
+Goal "x===y ==> y:D";
 by (etac (sym2refl2 RS DomainI) 1);
 qed "DomainI_right"; 
 
-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);by (assume_tac 1);
+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 (fast_tac set_cs 1);
+by (Blast_tac 1);
 qed "notDomainE1"; 
 
-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);by (assume_tac 1);
+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 (fast_tac set_cs 1);
+by (Blast_tac 1);
 qed "notDomainE2"; 
 
 (* theorems for equivalence relations *)
@@ -94,16 +86,12 @@
 qed "er_Domain";
 
 (* witnesses for "=>" ::(per,per)per  *)
-val prems = goalw thy [fun_per_def]"eqv (x::'a::per => 'b::per) y ==> eqv y x";
-by (cut_facts_tac prems 1);
-by (safe_tac HOL_cs);
-by (asm_full_simp_tac (HOL_ss addsimps [per_sym2]) 1);
+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";
 
-val prems = goalw thy [fun_per_def]
-	"[| eqv (f::'a::per=>'b::per) g;eqv g h|] ==> eqv f h";
-by (cut_facts_tac prems 1);
-by (safe_tac HOL_cs);
+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);