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/HOLCF/IOA/meta_theory/TL.thy
changeset 12028 52aa183c15bb
parent 10835 f4745d77e620
child 12114 a8e860c86252
equal deleted inserted replaced
12027:1281e9bf57f6 12028:52aa183c15bb 
    43 defs
 
    43 defs
 
    44 
    44 
    45 
    45 
    46 unlift_def
 
    46 unlift_def
 
    47   "unlift x == (case x of 
    47   "unlift x == (case x of 
    48                  Undef   => arbitrary
 
    48                  UU   => arbitrary
 
    49                | Def y   => y)"
 
    49                | Def y   => y)"
 
    50 
    50 
    51 (* this means that for nil and UU the effect is unpredictable *)
 
    51 (* this means that for nil and UU the effect is unpredictable *)
 
    52 Init_def
 
    52 Init_def
 
    53   "Init P s ==  (P (unlift (HD$s)))" 
    53   "Init P s ==  (P (unlift (HD$s)))"
isabelle