Mercurial Mercurial > repos > isabelle / file revision
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/ex/Witness.thy
author oheimb
Fri, 31 Jan 1997 16:56:32 +0100
changeset 2570 24d7e8fb8261
child 2642 3c3a84cc85a9
permissions -rw-r--r--
added Classlib.* and Witness.*, moved (and updated) Coind.*, Dagstuhl.*, Dlist.*, Dnat.*, Focus_ex.* and Stream.* from HOLCF/explicit_domains to here adapted several proofs; now they work again. Hope that the following strange errors (when committing) do not matter: rlog error: RCS/Classlib.ML,v: No such file or directory rlog error: RCS/Classlib.thy,v: No such file or directory rlog error: RCS/Coind.ML,v: No such file or directory rlog error: RCS/Coind.thy,v: No such file or directory rlog error: RCS/Dagstuhl.ML,v: No such file or directory rlog error: RCS/Dagstuhl.thy,v: No such file or directory rlog error: RCS/Dlist.ML,v: No such file or directory rlog error: RCS/Dlist.thy,v: No such file or directory rlog error: RCS/Dnat.ML,v: No such file or directory rlog error: RCS/Dnat.thy,v: No such file or directory rlog error: RCS/Focus_ex.ML,v: No such file or directory rlog error: RCS/Focus_ex.thy,v: No such file or directory rlog error: RCS/Stream.ML,v: No such file or directory rlog error: RCS/Stream.thy,v: No such file or directory rlog error: RCS/Witness.ML,v: No such file or directory rlog error: RCS/Witness.thy,v: No such file or directory

(*  Title:      FOCUS/Witness.thy
    ID:         $ $
    Author:     Franz Regensburger
    Copyright   1995 Technical University Munich

Witnesses for introduction of type cleasse in theory Classlib

The 8bit package is needed for this theory

The type void of HOLCF/Void.thy is a witness for all the introduced classes.

the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
the trivial instance for .= and .<=  is LAM x y.(UU::tr)

*)

Witness = HOLCF +

ops curried 
	"circ"	:: "void -> void -> void"		(cinfixl 65)
	"bullet":: "void -> void -> tr"			(cinfixl 55)

defs 

circ_def	"(op circ) Ú (LAM x y.UU)"

bullet_def	"(op bullet) Ú (LAM x y.UU)"

end
isabelle