src/CCL/ex/Nat.thy
changeset 24825 c4f13ab78f9d
parent 20140 98acc6d0fab6
child 27221 31328dc30196
equal deleted inserted replaced
24824:b7866aea0815 24825:c4f13ab78f9d
    11 begin
    11 begin
    12 
    12 
    13 consts
    13 consts
    14 
    14 
    15   not   :: "i=>i"
    15   not   :: "i=>i"
    16   "#+"  :: "[i,i]=>i"            (infixr 60)
    16   add   :: "[i,i]=>i"            (infixr "#+" 60)
    17   "#*"  :: "[i,i]=>i"            (infixr 60)
    17   mult  :: "[i,i]=>i"            (infixr "#*" 60)
    18   "#-"  :: "[i,i]=>i"            (infixr 60)
    18   sub   :: "[i,i]=>i"            (infixr "#-" 60)
    19   "##"  :: "[i,i]=>i"            (infixr 60)
    19   div   :: "[i,i]=>i"            (infixr "##" 60)
    20   "#<"  :: "[i,i]=>i"            (infixr 60)
    20   lt    :: "[i,i]=>i"            (infixr "#<" 60)
    21   "#<=" :: "[i,i]=>i"            (infixr 60)
    21   le    :: "[i,i]=>i"            (infixr "#<=" 60)
    22   ackermann :: "[i,i]=>i"
    22   ackermann :: "[i,i]=>i"
    23 
    23 
    24 defs
    24 defs
    25 
    25 
    26   not_def:     "not(b) == if b then false else true"
    26   not_def:     "not(b) == if b then false else true"