Records:
- Record types are now by default printed with their type abbreviation
instead of the list of all field types. This can be configured via
the reference "print_record_type_abbr".
- Simproc "record_upd_simproc" for simplification of multiple updates
added (not enabled by default).
- Tactic "record_split_simp_tac" to split and simplify records added.
- Bug-fix and optimisation of "record_simproc".
- "record_simproc" and "record_upd_simproc" are now sensitive to
quick_and_dirty flag.
(* Title: HOL/MiniML/MiniML.thy
ID: $Id$
Author: Wolfgang Naraschewski and Tobias Nipkow
Copyright 1996 TU Muenchen
Mini_ML with type inference rules.
*)
MiniML = Generalize +
(* expressions *)
datatype
expr = Var nat | Abs expr | App expr expr | LET expr expr
(* type inference rules *)
consts
has_type :: "(ctxt * expr * typ)set"
syntax
"@has_type" :: [ctxt, expr, typ] => bool
("((_) |-/ (_) :: (_))" [60,0,60] 60)
translations
"A |- e :: t" == "(A,e,t):has_type"
inductive has_type
intrs
VarI "[| n < length A; t <| A!n |] ==> A |- Var n :: t"
AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2"
AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |]
==> A |- App e1 e2 :: t1"
LETI "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t"
end