# HG changeset patch
# User paulson
# Date 881142342 -3600
# Node ID d683b7898c6186ead7f0476ba560a63a9f044f63
# Parent  15fab62268c32fd18025aafe6793450bbd0ddc73
Miniscoping now used except for one proof

diff -r 15fab62268c3 -r d683b7898c61 src/CCL/CCL.ML
--- a/src/CCL/CCL.ML	Tue Dec 02 12:42:59 1997 +0100
+++ b/src/CCL/CCL.ML	Wed Dec 03 10:45:42 1997 +0100
@@ -10,7 +10,7 @@
 
 val ccl_data_defs = [apply_def,fix_def];
 
-val CCL_ss = set_ss addsimps [po_refl RS P_iff_T];
+val CCL_ss = set_ss addsimps [po_refl];
 
 (*** Congruence Rules ***)
 
@@ -155,17 +155,17 @@
 qed "POgen_mono";
 
 goalw CCL.thy [POgen_def,SIM_def]
-  "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
-\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
-\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))";
+ "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
+\          (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
+\          (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))";
 by (rtac (iff_refl RS XHlemma2) 1);
 qed "POgenXH";
 
 goal CCL.thy
   "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
-\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
-\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
-by (simp_tac (ccl_ss addsimps [PO_iff]) 1);
+\                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
+\                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
+by (simp_tac (ccl_ss addsimps [PO_iff] delsimps ex_simps) 1);
 br (rewrite_rule [POgen_def,SIM_def] 
                  (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
 by (rtac (iff_refl RS XHlemma2) 1);
@@ -186,7 +186,6 @@
 goal CCL.thy "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
 by (rtac (poXH RS iff_trans) 1);
 by (simp_tac ccl_ss 1);
-by (fast_tac ccl_cs 1);
 qed "po_pair";
 
 goal CCL.thy "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
diff -r 15fab62268c3 -r d683b7898c61 src/CCL/subset.ML
--- a/src/CCL/subset.ML	Tue Dec 02 12:42:59 1997 +0100
+++ b/src/CCL/subset.ML	Wed Dec 03 10:45:42 1997 +0100
@@ -120,5 +120,4 @@
 val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong];
 
 val set_ss = FOL_ss addcongs set_congs
-                    delsimps (ex_simps @ all_simps)  (*NO miniscoping*)
                     addsimps mem_rews;