src/HOL/MiniML/MiniML.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 4502 337c073de95e
child 14422 b8da5f258b04
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* Title:     HOL/MiniML/MiniML.thy
     2    ID:        $Id$
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1996 TU Muenchen
     5 
     6 Mini_ML with type inference rules.
     7 *)
     8 
     9 MiniML = Generalize + 
    10 
    11 (* expressions *)
    12 datatype
    13         expr = Var nat | Abs expr | App expr expr | LET expr expr
    14 
    15 (* type inference rules *)
    16 consts
    17         has_type :: "(ctxt * expr * typ)set"
    18 syntax
    19         "@has_type" :: [ctxt, expr, typ] => bool
    20                        ("((_) |-/ (_) :: (_))" [60,0,60] 60)
    21 translations 
    22         "A |- e :: t" == "(A,e,t):has_type"
    23 
    24 inductive has_type
    25 intrs
    26         VarI "[| n < length A; t <| A!n |] ==> A |- Var n :: t"
    27         AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2"
    28         AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] 
    29               ==> A |- App e1 e2 :: t1"
    30         LETI "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t"
    31 
    32 end