src/HOL/Bali/Basis.thy
changeset 30235 58d147683393
parent 27239 f2f42f9fa09d
child 32149 ef59550a55d3
     1.1 --- a/src/HOL/Bali/Basis.thy	Tue Mar 03 17:05:18 2009 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Wed Mar 04 10:47:20 2009 +0100
     1.3 @@ -251,8 +251,8 @@
     1.4    Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
     1.5  
     1.6  translations
     1.7 -  "! x:A: P"    == "! x:o2s A. P"
     1.8 -  "? x:A: P"    == "? x:o2s A. P"
     1.9 +  "! x:A: P"    == "! x:CONST Option.set A. P"
    1.10 +  "? x:A: P"    == "? x:CONST Option.set A. P"
    1.11  
    1.12  section "Special map update"
    1.13