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/Tr2.thy
author lcp
Thu, 12 Jan 1995 03:03:45 +0100
changeset 857 f5314a7c93f2
parent 752 b89462f9d5f1
child 1168 74be52691d62
permissions -rw-r--r--
Renamed single_fun to singleton_fun.

(*  Title: 	HOLCF/tr2.thy
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen

Introduce infix if_then_else_fi and boolean connectives andalso, orelse
*)

Tr2 = Tr1 +

consts
	Icifte		:: "tr -> 'c -> 'c -> 'c"
	trand		:: "tr -> tr -> tr"
	tror		:: "tr -> tr -> tr"
        neg		:: "tr -> tr"

syntax 	"@cifte"	:: "tr=>'c=>'c=>'c"
                             ("(3If _/ (then _/ else _) fi)" 60)
	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [36,35] 35)
	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
 
translations "x andalso y" == "trand[x][y]"
             "x orelse y"  == "tror[x][y]"
             "If b then e1 else e2 fi" == "Icifte[b][e1][e2]"
              
rules

  ifte_def    "Icifte == (LAM t e1 e2.tr_when[e1][e2][t])"
  andalso_def "trand == (LAM t1 t2.tr_when[t2][FF][t1])"
  orelse_def  "tror  == (LAM t1 t2.tr_when[TT][t2][t1])"
  neg_def     "neg == (LAM t. tr_when[FF][TT][t])"

end
isabelle