changeset 1376 | 92f83b9d17e1 |
parent 1300 | c7a8f374339b |
child 1400 | 5d909faf0e04 |
--- a/src/HOL/MiniML/MiniML.thy Thu Nov 30 12:58:44 1995 +0100 +++ b/src/HOL/MiniML/MiniML.thy Fri Dec 01 12:03:13 1995 +0100 @@ -16,7 +16,7 @@ consts has_type :: "(type_expr list * expr * type_expr)set" syntax - "@has_type" :: "[type_expr list, expr, type_expr] => bool" + "@has_type" :: [type_expr list, expr, type_expr] => bool ("((_) |-/ (_) :: (_))" 60) translations "a |- e :: t" == "(a,e,t):has_type"