src/HOL/ex/Eval_examples.thy
changeset 23134 6cd88d27f600
parent 22804 d3c23b90c6c6
equal deleted inserted replaced
23133:5a6935d598c3 23134:6cd88d27f600
    18 value (overloaded) "(Suc 2 + 1) * 4"
    18 value (overloaded) "(Suc 2 + 1) * 4"
    19 value (overloaded) "(Suc 2 + 1) * 4"
    19 value (overloaded) "(Suc 2 + 1) * 4"
    20 value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
    20 value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
    21 value (overloaded) "[]::nat list"
    21 value (overloaded) "[]::nat list"
    22 value (overloaded) "fst ([]::nat list, Suc 0) = []"
    22 value (overloaded) "fst ([]::nat list, Suc 0) = []"
       
    23 value (overloaded) "nat 100"
       
    24 value (overloaded) "[(nat 100, ())]"
       
    25 value (overloaded) "int 10 \<le> 12"
    23 
    26 
    24 text {* a fancy datatype *}
    27 text {* a fancy datatype *}
    25 
    28 
    26 datatype ('a, 'b) bair =
    29 datatype ('a, 'b) bair =
    27     Bair "'a\<Colon>order" 'b
    30     Bair "'a\<Colon>order" 'b