isabelle: src/HOL/MiniML/MiniML.thy@03a843f0f447 (annotated)

1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	1	(* Title: HOL/MiniML/MiniML.thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	2	ID: $Id$
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	3	Author: Dieter Nazareth and Tobias Nipkow
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	5
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	6	Mini_ML with type inference rules.
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	7	*)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	8
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	9	MiniML = Type +
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	10
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	11	(* expressions *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	12	datatype
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1400 diff changeset	13	expr = Var nat \| Abs expr \| App expr expr
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	14
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	15	(* type inference rules *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	16	consts
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1400 diff changeset	17	has_type :: "(typ list * expr * typ)set"
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	18	syntax
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	19	"@has_type" :: [typ list, expr, typ] => bool
1525 d127436567d0 modified priorities in syntax nipkow parents: 1476 diff changeset	20	("((_) \|-/ (_) :: (_))" [60,0,60] 60)
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	21	translations
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	22	"a \|- e :: t" == "(a,e,t):has_type"
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	23
1790 2f3694c50101 Quotes now optional around inductive set paulson parents: 1525 diff changeset	24	inductive has_type
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	25	intrs
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1400 diff changeset	26	VarI "[\| n < length a \|] ==> a \|- Var n :: nth n a"
608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1400 diff changeset	27	AbsI "[\| t1#a \|- e :: t2 \|] ==> a \|- Abs e :: t1 -> t2"
608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1400 diff changeset	28	AppI "[\| a \|- e1 :: t2 -> t1; a \|- e2 :: t2 \|]
608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1400 diff changeset	29	==> a \|- App e1 e2 :: t1"
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	30
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	31	end
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	32

author	paulson
	Thu, 26 Sep 1996 12:47:47 +0200
changeset 2031	03a843f0f447
parent 1790	2f3694c50101
child 2525	477c05586286
permissions	-rw-r--r--