src/HOL/TLA/Stfun.thy
changeset 60587 0318b43ee95c
parent 58889 5b7a9633cfa8
child 60588 750c533459b1
     1.1 --- a/src/HOL/TLA/Stfun.thy	Fri Jun 26 11:07:04 2015 +0200
     1.2 +++ b/src/HOL/TLA/Stfun.thy	Fri Jun 26 11:44:22 2015 +0200
     1.3 @@ -50,13 +50,13 @@
     1.4    basevars_def:  "stvars vs == range vs = UNIV"
     1.5  
     1.6  
     1.7 -lemma basevars: "!!vs. basevars vs ==> EX u. vs u = c"
     1.8 +lemma basevars: "\<And>vs. basevars vs ==> \<exists>u. vs u = c"
     1.9    apply (unfold basevars_def)
    1.10    apply (rule_tac b = c and f = vs in rangeE)
    1.11     apply auto
    1.12    done
    1.13  
    1.14 -lemma base_pair1: "!!x y. basevars (x,y) ==> basevars x"
    1.15 +lemma base_pair1: "\<And>x y. basevars (x,y) ==> basevars x"
    1.16    apply (simp (no_asm) add: basevars_def)
    1.17    apply (rule equalityI)
    1.18     apply (rule subset_UNIV)
    1.19 @@ -65,7 +65,7 @@
    1.20    apply auto
    1.21    done
    1.22  
    1.23 -lemma base_pair2: "!!x y. basevars (x,y) ==> basevars y"
    1.24 +lemma base_pair2: "\<And>x y. basevars (x,y) ==> basevars y"
    1.25    apply (simp (no_asm) add: basevars_def)
    1.26    apply (rule equalityI)
    1.27     apply (rule subset_UNIV)
    1.28 @@ -74,7 +74,7 @@
    1.29    apply auto
    1.30    done
    1.31  
    1.32 -lemma base_pair: "!!x y. basevars (x,y) ==> basevars x & basevars y"
    1.33 +lemma base_pair: "\<And>x y. basevars (x,y) ==> basevars x & basevars y"
    1.34    apply (rule conjI)
    1.35    apply (erule base_pair1)
    1.36    apply (erule base_pair2)
    1.37 @@ -89,7 +89,7 @@
    1.38    apply auto
    1.39    done
    1.40  
    1.41 -lemma baseE: "[| basevars v; !!x. v x = c ==> Q |] ==> Q"
    1.42 +lemma baseE: "[| basevars v; \<And>x. v x = c ==> Q |] ==> Q"
    1.43    apply (erule basevars [THEN exE])
    1.44    apply blast
    1.45    done
    1.46 @@ -99,7 +99,7 @@
    1.47     The following shows that there should not be duplicates in a "stvars" tuple:
    1.48  *)
    1.49  
    1.50 -lemma "!!v. basevars (v::bool stfun, v) ==> False"
    1.51 +lemma "\<And>v. basevars (v::bool stfun, v) ==> False"
    1.52    apply (erule baseE)
    1.53    apply (subgoal_tac "(LIFT (v,v)) x = (True, False)")
    1.54     prefer 2