--- a/Admin/Benchmarks/HOL-datatype/Brackin.thy Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Brackin.thy Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-Brackin = Main +
+theory Brackin = Main:
(* ------------------------------------------------------------------------- *)
(* A couple from Steve Brackin's work. *)
@@ -16,31 +16,31 @@
datatype
('a, 'b, 'c) TY1 =
NoF__
- | Fk__ 'a (('a, 'b, 'c) TY2)
+ | Fk__ 'a "('a, 'b, 'c) TY2"
and
('a, 'b, 'c) TY2 =
Ta__ bool
| Td__ bool
- | Tf__ (('a, 'b, 'c) TY1)
+ | 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)
+ | 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)
+ | 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)
+ | 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