# HG changeset patch
# User wenzelm
# Date 876730948 -7200
# Node ID d5905b98291fba97ff335d5d5ab354aa3308c64a
# Parent  6061fa4637848b004318c2c1d5ab58dfdc95b758
fixed dots;

diff -r 6061fa463784 -r d5905b98291f src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Oct 13 10:22:28 1997 +0200
@@ -65,7 +65,7 @@
    "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
 \     move A (@x. move A x (f s) a (f t)) (f s) a (f t)";
 
-by (subgoal_tac "? ex.move A ex (f s) a (f t)" 1);
+by (subgoal_tac "? ex. move A ex (f s) a (f t)" 1);
 by (Asm_full_simp_tac 2);
 by (etac exE 1);
 by (rtac selectI 1);
diff -r 6061fa463784 -r d5905b98291f src/HOLCF/IOA/meta_theory/Seq.ML
--- a/src/HOLCF/IOA/meta_theory/Seq.ML	Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Mon Oct 13 10:22:28 1997 +0200
@@ -74,7 +74,7 @@
 qed"sfilter_UU";
 
 goal thy 
-"!!x.x~=UU ==> sfilter`P`(x##xs)=   \
+"!!x. x~=UU ==> sfilter`P`(x##xs)=   \
 \             (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
 by (rtac trans 1);
 by (stac sfilter_unfold 1);
@@ -102,7 +102,7 @@
 qed"sforall2_UU";
 
 goal thy 
-"!!x.x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
+"!!x. x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
 by (rtac trans 1);
 by (stac sforall2_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -131,7 +131,7 @@
 qed"stakewhile_UU";
 
 goal thy 
-"!!x.x~=UU ==> stakewhile`P`(x##xs) =   \
+"!!x. x~=UU ==> stakewhile`P`(x##xs) =   \
 \             (If P`x then x##(stakewhile`P`xs) else nil fi)";
 by (rtac trans 1);
 by (stac stakewhile_unfold 1);
@@ -160,7 +160,7 @@
 qed"sdropwhile_UU";
 
 goal thy 
-"!!x.x~=UU ==> sdropwhile`P`(x##xs) =   \
+"!!x. x~=UU ==> sdropwhile`P`(x##xs) =   \
 \             (If P`x then sdropwhile`P`xs else x##xs fi)";
 by (rtac trans 1);
 by (stac sdropwhile_unfold 1);
@@ -191,7 +191,7 @@
 qed"slast_UU";
 
 goal thy 
-"!!x.x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
+"!!x. x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
 by (rtac trans 1);
 by (stac slast_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -288,7 +288,7 @@
 by (REPEAT (Asm_full_simp_tac 1));
 qed"szip_UU2";
 
-goal thy "!!x.x~=UU ==> szip`(x##xs)`nil=UU";
+goal thy "!!x. x~=UU ==> szip`(x##xs)`nil=UU";
 by (rtac trans 1);
 by (stac szip_unfold 1);
 by (REPEAT (Asm_full_simp_tac 1));
@@ -417,7 +417,7 @@
 by (fast_tac (HOL_cs addSDs seq.injects) 1);
 qed"Finite_cons_a";
 
-goal thy "!!x.a~=UU ==>(Finite (a##x)) = (Finite x)";
+goal thy "!!x. a~=UU ==>(Finite (a##x)) = (Finite x)";
 by (rtac iffI 1);
 by (rtac (Finite_cons_a RS mp RS mp RS mp) 1);
 by (REPEAT (assume_tac 1));
@@ -439,7 +439,7 @@
 
 
 qed_goalw "seq_finite_ind_lemma" thy  [seq.finite_def]
-"(!!n.P(seq_take n`s)) ==>  seq_finite(s) -->P(s)"
+"(!!n. P(seq_take n`s)) ==>  seq_finite(s) -->P(s)"
  (fn prems =>
         [
         (strip_tac 1),
diff -r 6061fa463784 -r d5905b98291f src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Mon Oct 13 10:22:28 1997 +0200
@@ -106,7 +106,7 @@
 
 
 proj_def 
- "nproj == (%n tr.HD`(iterate n TL tr))"   
+ "nproj == (%n tr. HD`(iterate n TL tr))"   
 
 Partial_def
   "Partial x  == (seq_finite x) & ~(Finite x)"
diff -r 6061fa463784 -r d5905b98291f src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Mon Oct 13 10:22:28 1997 +0200
@@ -95,7 +95,7 @@
 
 goal thy "Filter P`s = Filter P`(Cut P s)";
 
-by (res_inst_tac [("A1","%x.True")
+by (res_inst_tac [("A1","%x. True")
                  ,("Q1","%x.~ P x"), ("x1","s")]
                  (take_lemma_induct RS mp) 1);
 by (Fast_tac 3);
@@ -112,7 +112,7 @@
 
 goal thy "Cut P (Cut P s) = (Cut P s)";
 
-by (res_inst_tac [("A1","%x.True")
+by (res_inst_tac [("A1","%x. True")
                  ,("Q1","%x.~ P x"), ("x1","s")]
                  (take_lemma_less_induct RS mp) 1);
 by (Fast_tac 3);
@@ -130,7 +130,7 @@
 
 goal thy "Map f`(Cut (P o f) s) = Cut P (Map f`s)";
 
-by (res_inst_tac [("A1","%x.True")
+by (res_inst_tac [("A1","%x. True")
                  ,("Q1","%x.~ P (f x)"), ("x1","s")]
                  (take_lemma_less_induct RS mp) 1);
 by (Fast_tac 3);
@@ -230,17 +230,17 @@
 
 
 goalw thy [schedules_def,has_schedule_def]
- "!! sch. [|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|] \
+ "!! sch. [|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
 \   ==> ? sch. sch : schedules A & \
-\              tr = Filter (%a.a:ext A)`sch &\
+\              tr = Filter (%a. a:ext A)`sch &\
 \              LastActExtsch A sch";
 
 by (safe_tac set_cs);
-by (res_inst_tac [("x","filter_act`(Cut (%a.fst a:ext A) (snd ex))")] exI 1);
+by (res_inst_tac [("x","filter_act`(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
 by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
 by (pair_tac "ex" 1);
 by (safe_tac set_cs);
-by (res_inst_tac [("x","(x,Cut (%a.fst a:ext A) y)")] exI 1);
+by (res_inst_tac [("x","(x,Cut (%a. fst a:ext A) y)")] exI 1);
 by (Asm_simp_tac 1);
 
 (* Subgoal 1: Lemma:  propagation of execution through Cut *)
@@ -250,14 +250,14 @@
 (* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
 
 by (simp_tac (!simpset addsimps [filter_act_def]) 1);
-by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
+by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
 by (rtac (rewrite_rule [o_def] MapCut) 2);
 by (asm_full_simp_tac (!simpset addsimps [FilterCut RS sym]) 1);
 
 (* Subgoal 3: Lemma: Cut idempotent  *)
 
 by (simp_tac (!simpset addsimps [LastActExtsch_def,filter_act_def]) 1);
-by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
+by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
 by (rtac (rewrite_rule [o_def] MapCut) 2);
 by (asm_full_simp_tac (!simpset addsimps [Cut_idemp]) 1);
 qed"exists_LastActExtsch";
@@ -268,7 +268,7 @@
 (* ---------------------------------------------------------------- *)
 
 goalw  thy [LastActExtsch_def]
-  "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = nil |] \
+  "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
 \   ==> sch=nil";
 by (dtac FilternPnilForallP 1);
 by (etac conjE 1);
@@ -278,7 +278,7 @@
 qed"LastActExtimplnil";
 
 goalw  thy [LastActExtsch_def]
-  "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = UU |] \
+  "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
 \   ==> sch=UU";
 by (dtac FilternPUUForallP 1);
 by (etac conjE 1);
diff -r 6061fa463784 -r d5905b98291f src/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Mon Oct 13 10:22:28 1997 +0200
@@ -25,7 +25,7 @@
 defs
 
 LastActExtsch_def
-  "LastActExtsch A sch == (Cut (%x.x: ext A) sch = sch)"
+  "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"
 
 LastActExtex_def
   "LastActExtex A ex == LastActExtsch A (filter_act`ex)"