src/ZF/Constructible/L_axioms.thy
changeset 69587 53982d5ec0bb
parent 61798 27f3c10b0b50
child 69593 3dda49e08b9d
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Jan 03 21:06:39 2019 +0100
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Jan 03 21:15:52 2019 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4  text\<open>We must use the meta-existential quantifier; otherwise the reflection
     1.5        terms become enormous!\<close>
     1.6  definition
     1.7 -  L_Reflects :: "[i=>o,[i,i]=>o] => prop"  ("(3REFLECTS/ [_,/ _])") where
     1.8 +  L_Reflects :: "[i=>o,[i,i]=>o] => prop"  (\<open>(3REFLECTS/ [_,/ _])\<close>) where
     1.9      "REFLECTS[P,Q] == (\<Or>Cl. Closed_Unbounded(Cl) &
    1.10                             (\<forall>a. Cl(a) \<longrightarrow> (\<forall>x \<in> Lset(a). P(x) \<longleftrightarrow> Q(a,x))))"
    1.11  
    1.12 @@ -268,25 +268,25 @@
    1.13  subsubsection\<open>Some numbers to help write de Bruijn indices\<close>
    1.14  
    1.15  abbreviation
    1.16 -  digit3 :: i   ("3") where "3 == succ(2)"
    1.17 +  digit3 :: i   (\<open>3\<close>) where "3 == succ(2)"
    1.18  
    1.19  abbreviation
    1.20 -  digit4 :: i   ("4") where "4 == succ(3)"
    1.21 +  digit4 :: i   (\<open>4\<close>) where "4 == succ(3)"
    1.22  
    1.23  abbreviation
    1.24 -  digit5 :: i   ("5") where "5 == succ(4)"
    1.25 +  digit5 :: i   (\<open>5\<close>) where "5 == succ(4)"
    1.26  
    1.27  abbreviation
    1.28 -  digit6 :: i   ("6") where "6 == succ(5)"
    1.29 +  digit6 :: i   (\<open>6\<close>) where "6 == succ(5)"
    1.30  
    1.31  abbreviation
    1.32 -  digit7 :: i   ("7") where "7 == succ(6)"
    1.33 +  digit7 :: i   (\<open>7\<close>) where "7 == succ(6)"
    1.34  
    1.35  abbreviation
    1.36 -  digit8 :: i   ("8") where "8 == succ(7)"
    1.37 +  digit8 :: i   (\<open>8\<close>) where "8 == succ(7)"
    1.38  
    1.39  abbreviation
    1.40 -  digit9 :: i   ("9") where "9 == succ(8)"
    1.41 +  digit9 :: i   (\<open>9\<close>) where "9 == succ(8)"
    1.42  
    1.43  
    1.44  subsubsection\<open>The Empty Set, Internalized\<close>