src/HOL/Modelcheck/MuckeSyn.thy
changeset 21524 7843e2fd14a9
parent 17272 c63e5220ed77
child 22819 a7b425bb668c
equal deleted inserted replaced
21523:a267ecd51f90 21524:7843e2fd14a9
    27   "op |"        :: "[bool, bool] => bool"               (infixr "|" 30)
    27   "op |"        :: "[bool, bool] => bool"               (infixr "|" 30)
    28   "op -->"      :: "[bool, bool] => bool"               (infixr "->" 25)
    28   "op -->"      :: "[bool, bool] => bool"               (infixr "->" 25)
    29   "op ="        :: "['a, 'a] => bool"                   ("(_ =/ _)" [51, 51] 50)
    29   "op ="        :: "['a, 'a] => bool"                   ("(_ =/ _)" [51, 51] 50)
    30   "_not_equal"  :: "['a, 'a] => bool"                   ("(_ !=/ _)" [51, 51] 50)
    30   "_not_equal"  :: "['a, 'a] => bool"                   ("(_ !=/ _)" [51, 51] 50)
    31 
    31 
    32   "ALL "        :: "[idts, bool] => bool"               ("'((3forall _./ _)')" [0, 10] 10)
    32   All_binder    :: "[idts, bool] => bool"               ("'((3forall _./ _)')" [0, 10] 10)
    33   "EX "         :: "[idts, bool] => bool"               ("'((3exists _./ _)')" [0, 10] 10)
    33   Ex_binder     :: "[idts, bool] => bool"               ("'((3exists _./ _)')" [0, 10] 10)
    34 
    34 
    35   "_lambda"     :: "[idts, 'a] => 'b"                   ("(3L _./ _)" 10)
    35   "_lambda"     :: "[idts, 'a] => 'b"                   ("(3L _./ _)" 10)
    36   "_applC"      :: "[('b => 'a), cargs] => aprop"       ("(1_/ '(_'))" [1000,1000] 999)
    36   "_applC"      :: "[('b => 'a), cargs] => aprop"       ("(1_/ '(_'))" [1000,1000] 999)
    37   "_cargs"      :: "['a, cargs] => cargs"               ("_,/ _" [1000,1000] 1000)
    37   "_cargs"      :: "['a, cargs] => cargs"               ("_,/ _" [1000,1000] 1000)
    38 
    38