isabelle: src/HOL/W0/Maybe.thy@1056cbbaeb29 (annotated)

2520 aecaa76e7eff Incorporated Larry's changes. nipkow parents: 2518 diff changeset	1	(* Title: HOL/W0/Maybe.thy
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	2	ID: $Id$
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	3	Author: Dieter Nazareth and Tobias Nipkow
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	5
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	6	Universal error monad.
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	7	*)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	8
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	9	Maybe = List +
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	10
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	11	datatype 'a maybe = Ok 'a \| Fail
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	12
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	13	constdefs
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	14	bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	15	"m bind f == case m of Ok r => f r \| Fail => Fail"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	16
3692 9f9bcce140ce tuned pattern syntax; wenzelm parents: 2520 diff changeset	17	syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
3842 b55686a7b22c fixed dots; wenzelm parents: 3692 diff changeset	18	translations "P := E; F" == "E bind (%P. F)"
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	19
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	20	end

author	oheimb
	Fri, 02 Jun 2000 17:46:32 +0200
changeset 9020	1056cbbaeb29
parent 3842	b55686a7b22c
permissions	-rw-r--r--