# HG changeset patch # User clasohm # Date 796386320 -7200 # Node ID 5d57287e5e1ec38d5e5fed84a8a76dd4bc74feff # Parent 14b55f7fbf1574bd009f6299785173d94502b269 changed syntax of datatype declarations (curried types for constructor parameters) diff -r 14b55f7fbf15 -r 5d57287e5e1e src/HOL/IMP/Com.thy --- a/src/HOL/IMP/Com.thy Tue Mar 28 12:21:10 1995 +0200 +++ b/src/HOL/IMP/Com.thy Tue Mar 28 12:25:20 1995 +0200 @@ -19,10 +19,10 @@ arities loc :: term datatype - aexp = N (nat) - | X (loc) - | Op1 (n2n, aexp) - | Op2 (n2n2n, aexp, aexp) + aexp = N nat + | X loc + | Op1 n2n aexp + | Op2 n2n2n aexp aexp (** Evaluation of arithmetic expressions **) consts evala :: "(aexp*state*nat)set" @@ -44,10 +44,10 @@ datatype bexp = true | false - | ROp (n2n2b, aexp, aexp) - | noti (bexp) - | andi (bexp,bexp) (infixl 60) - | ori (bexp,bexp) (infixl 60) + | ROp n2n2b aexp aexp + | noti bexp + | andi bexp bexp (infixl 60) + | ori bexp bexp (infixl 60) (** Evaluation of boolean expressions **) consts evalb :: "(bexp*state*bool)set" @@ -72,10 +72,10 @@ datatype com = skip - | ":=" (loc,aexp) (infixl 60) - | semic (com,com) ("_; _" [60, 60] 10) - | whileC (bexp,com) ("while _ do _" 60) - | ifC (bexp, com, com) ("ifc _ then _ else _" 60) + | ":=" loc aexp (infixl 60) + | semic com com ("_; _" [60, 60] 10) + | whileC bexp com ("while _ do _" 60) + | ifC bexp com com ("ifc _ then _ else _" 60) (** Execution of commands **) consts evalc :: "(com*state*state)set" diff -r 14b55f7fbf15 -r 5d57287e5e1e src/HOL/List.thy --- a/src/HOL/List.thy Tue Mar 28 12:21:10 1995 +0200 +++ b/src/HOL/List.thy Tue Mar 28 12:25:20 1995 +0200 @@ -9,7 +9,7 @@ List = Arith + -datatype 'a list = "[]" ("[]") | "#"('a,'a list) (infixr 65) +datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65) consts diff -r 14b55f7fbf15 -r 5d57287e5e1e src/HOL/ex/PropLog.thy --- a/src/HOL/ex/PropLog.thy Tue Mar 28 12:21:10 1995 +0200 +++ b/src/HOL/ex/PropLog.thy Tue Mar 28 12:25:20 1995 +0200 @@ -8,7 +8,7 @@ PropLog = Finite + datatype - 'a pl = false | var ('a) ("#_" [1000]) | "->" ('a pl,'a pl) (infixr 90) + 'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90) consts thms :: "'a pl set => 'a pl set" "|-" :: "['a pl set, 'a pl] => bool" (infixl 50) diff -r 14b55f7fbf15 -r 5d57287e5e1e src/HOL/ex/String.thy --- a/src/HOL/ex/String.thy Tue Mar 28 12:21:10 1995 +0200 +++ b/src/HOL/ex/String.thy Tue Mar 28 12:25:20 1995 +0200 @@ -11,7 +11,7 @@ | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F datatype - char = Char (nibble, nibble) + char = Char nibble nibble types string = "char list" diff -r 14b55f7fbf15 -r 5d57287e5e1e src/HOL/thy_syntax.ML --- a/src/HOL/thy_syntax.ML Tue Mar 28 12:21:10 1995 +0200 +++ b/src/HOL/thy_syntax.ML Tue Mar 28 12:25:20 1995 +0200 @@ -138,10 +138,12 @@ (*parsers*) val tvars = type_args >> map (cat "dtVar"); - val typ = + val complex_typ = tvars -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list) || type_var >> cat "dtVar"; - val opt_typs = optional ("(" $$-- list1 typ --$$ ")") []; + val simple_typ = ident>>(cat "dtTyp" o curry mk_pair "[]" o quote) || + type_var >> cat "dtVar"; + val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")")); val constructor = name -- opt_typs -- opt_mixfix; in val datatype_decl =