Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Eval_Examples.thy
changeset 24423 ae9cd0e92423
parent 24292 26ac9fe0e80e
child 24587 4f2cbf6e563f
equal deleted inserted replaced
24422:c0b5ff9e9e4d 24423:ae9cd0e92423 
    29 value (overloaded) "(Suc 2 + 1) * 4"
 
    29 value (overloaded) "(Suc 2 + 1) * 4"
 
    30 value (overloaded) "(Suc 2 + 1) * 4"
 
    30 value (overloaded) "(Suc 2 + 1) * 4"
 
    31 value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
 
    31 value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
 
    32 value (overloaded) "nat 100"
 
    32 value (overloaded) "nat 100"
 
    33 value (overloaded) "(10\<Colon>int) \<le> 12"
 
    33 value (overloaded) "(10\<Colon>int) \<le> 12"
 
       
    34 value (overloaded) "[]::nat list"
 
    34 value (overloaded) "[(nat 100, ())]"
 
    35 value (overloaded) "[(nat 100, ())]"
 
    35 value (overloaded) "[]::nat list"
 
       
    36 
    36 
    37 text {* a fancy datatype *}
 
    37 text {* a fancy datatype *}
 
    38 
    38 
    39 datatype ('a, 'b) bair =
 
    39 datatype ('a, 'b) bair =
 
    40     Bair "'a\<Colon>order" 'b
 
    40     Bair "'a\<Colon>order" 'b
isabelle