--- a/src/HOL/Prod.thy Mon Nov 27 13:44:56 1995 +0100
+++ b/src/HOL/Prod.thy Wed Nov 29 16:44:59 1995 +0100
@@ -14,7 +14,7 @@
(* type definition *)
consts
- Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
+ Pair_Rep :: ['a, 'b] => ['a, 'b] => bool
defs
Pair_Rep_def "Pair_Rep == (%a b. %x y. x=a & y=b)"
@@ -40,9 +40,9 @@
syntax
"@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))")
- "@pttrn" :: "[pttrn,pttrns] => pttrn" ("'(_,/_')")
- "" :: " pttrn => pttrns" ("_")
- "@pttrns" :: "[pttrn,pttrns] => pttrns" ("_,/_")
+ "@pttrn" :: [pttrn,pttrns] => pttrn ("'(_,/_')")
+ "" :: pttrn => pttrns ("_")
+ "@pttrns" :: [pttrn,pttrns] => pttrns ("_,/_")
translations
"(x, y, z)" == "(x, (y, z))"
@@ -69,7 +69,7 @@
unit = "{p. p = True}"
consts
- "()" :: "unit" ("'(')")
+ "()" :: unit ("'(')")
defs
Unity_def "() == Abs_Unit(True)"