--- a/src/HOL/Datatype_Benchmark/Brackin.thy Fri Apr 12 08:27:43 2013 +0200
+++ b/src/HOL/Datatype_Benchmark/Brackin.thy Fri Apr 12 12:20:51 2013 +0200
@@ -5,39 +5,37 @@
theory Brackin imports Main begin
-datatype T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
- X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
- X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
- X32 | X33 | X34
+datatype T =
+ X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
+ X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
+ X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
+ X32 | X33 | X34
-datatype
- ('a, 'b, 'c) TY1 =
- NoF__
- | Fk__ 'a "('a, 'b, 'c) TY2"
-and
- ('a, 'b, 'c) TY2 =
- Ta__ bool
- | Td__ bool
- | Tf__ "('a, 'b, 'c) TY1"
- | Tk__ bool
- | Tp__ bool
- | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
- | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
-and
- ('a, 'b, 'c) TY3 =
- NoS__
- | Fresh__ "('a, 'b, 'c) TY2"
- | Trustworthy__ 'a
- | PrivateKey__ 'a 'b 'c
- | PublicKey__ 'a 'b 'c
- | Conveyed__ 'a "('a, 'b, 'c) TY2"
- | Possesses__ 'a "('a, 'b, 'c) TY2"
- | Received__ 'a "('a, 'b, 'c) TY2"
- | Recognizes__ 'a "('a, 'b, 'c) TY2"
- | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
- | Sends__ 'a "('a, 'b, 'c) TY2" 'b
- | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
- | Believes__ 'a "('a, 'b, 'c) TY3"
- | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
+datatype ('a, 'b, 'c) TY1 =
+ NoF
+ | Fk 'a "('a, 'b, 'c) TY2"
+and ('a, 'b, 'c) TY2 =
+ Ta bool
+ | Td bool
+ | Tf "('a, 'b, 'c) TY1"
+ | Tk bool
+ | Tp bool
+ | App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
+ | Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
+and ('a, 'b, 'c) TY3 =
+ NoS
+ | Fresh "('a, 'b, 'c) TY2"
+ | Trustworthy 'a
+ | PrivateKey 'a 'b 'c
+ | PublicKey 'a 'b 'c
+ | Conveyed 'a "('a, 'b, 'c) TY2"
+ | Possesses 'a "('a, 'b, 'c) TY2"
+ | Received 'a "('a, 'b, 'c) TY2"
+ | Recognizes 'a "('a, 'b, 'c) TY2"
+ | NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
+ | Sends 'a "('a, 'b, 'c) TY2" 'b
+ | SharedSecret 'a "('a, 'b, 'c) TY2" 'b
+ | Believes 'a "('a, 'b, 'c) TY3"
+ | And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
end