src/HOL/ex/Meson_Test.thy
changeset 39019 e46e7a9cb622
parent 37777 22107b894e5a
child 39093 4abe644fcea5
equal deleted inserted replaced
39009:95df565aceb7 39019:e46e7a9cb622
     8 text {*
     8 text {*
     9   WARNING: there are many potential conflicts between variables used
     9   WARNING: there are many potential conflicts between variables used
    10   below and constants declared in HOL!
    10   below and constants declared in HOL!
    11 *}
    11 *}
    12 
    12 
    13 hide_const (open) subset quotient union inter sum
    13 hide_const (open) implies union inter subset sum quotient 
    14 
    14 
    15 text {*
    15 text {*
    16   Test data for the MESON proof procedure
    16   Test data for the MESON proof procedure
    17   (Excludes the equality problems 51, 52, 56, 58)
    17   (Excludes the equality problems 51, 52, 56, 58)
    18 *}
    18 *}