src/HOL/Set.thy
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Set.thy	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4    val All_binder = Syntax.binder_name @{const_syntax All};
     1.5    val Ex_binder = Syntax.binder_name @{const_syntax Ex};
     1.6    val impl = @{const_syntax HOL.implies};
     1.7 -  val conj = @{const_syntax "op &"};
     1.8 +  val conj = @{const_syntax HOL.conj};
     1.9    val sbset = @{const_syntax subset};
    1.10    val sbset_eq = @{const_syntax subset_eq};
    1.11  
    1.12 @@ -269,7 +269,7 @@
    1.13      fun setcompr_tr [e, idts, b] =
    1.14        let
    1.15          val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
    1.16 -        val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
    1.17 +        val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
    1.18          val exP = ex_tr [idts, P];
    1.19        in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
    1.20  
    1.21 @@ -288,7 +288,7 @@
    1.22    fun setcompr_tr' [Abs (abs as (_, _, P))] =
    1.23      let
    1.24        fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
    1.25 -        | check (Const (@{const_syntax "op &"}, _) $
    1.26 +        | check (Const (@{const_syntax HOL.conj}, _) $
    1.27                (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
    1.28              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
    1.29              subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
    1.30 @@ -305,7 +305,7 @@
    1.31            val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
    1.32          in
    1.33            case t of
    1.34 -            Const (@{const_syntax "op &"}, _) $
    1.35 +            Const (@{const_syntax HOL.conj}, _) $
    1.36                (Const (@{const_syntax Set.member}, _) $
    1.37                  (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
    1.38              if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M