Mercurial Mercurial > repos > isabelle / annotate
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/explicit_domains/Dagstuhl.thy
author regensbu
Fri, 06 Oct 1995 17:25:24 +0100
changeset 1274 ea0668a1c0ba
child 1479 21eb5e156d91
permissions -rw-r--r--
added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset 
     1
 
(* $Id$ *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset 
     2
 












ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




     3














ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




     4


Dagstuhl  =  Stream2 +













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




     5














ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




     6


consts













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




     7


	y  :: "'a"













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




     8


       YS  :: "'a stream"













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




     9


       YYS :: "'a stream"













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    10














ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    11


defs













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    12














ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    13


YS_def    "YS  == fix`(LAM x. scons`y`x)"













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    14


YYS_def   "YYS == fix`(LAM z. scons`y`(scons`y`z))"













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    15


  













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    16


end













ea0668a1c0ba
added 8bit pragmas



regensbu


parents: 

diff
changeset




    17
















isabelle