isabelle: src/HOL/W0/Maybe.thy@36b28f78ed1b (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	paulson
	Wed, 03 Dec 1997 10:50:02 +0100
changeset 4351	36b28f78ed1b
parent 3842	b55686a7b22c
permissions	-rw-r--r--