# HG changeset patch
# User wenzelm
# Date 849109875 -3600
# Node ID b59781f2b809379c5eb4744238c02b6e2d979e91
# Parent  e6d738f2b9a9ae0b9b1649dc0b292e67a762b687
added symbols syntax;

diff -r e6d738f2b9a9 -r b59781f2b809 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Nov 27 16:48:19 1996 +0100
+++ b/src/HOL/HOL.thy	Wed Nov 27 16:51:15 1996 +0100
@@ -3,23 +3,17 @@
     Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
 
-Higher-Order Logic
+Higher-Order Logic.
 *)
 
 HOL = CPure +
 
+
+(** Core syntax **)
+
 classes
   term < logic
 
-axclass
-  plus < term
-
-axclass
-  minus < term
-
-axclass
-  times < term
-
 default
   term
 
@@ -57,13 +51,27 @@
   "|"           :: [bool, bool] => bool             (infixr 30)
   "-->"         :: [bool, bool] => bool             (infixr 25)
 
-  (* Overloaded Constants *)
+
+(* Overloaded Constants *)
+
+axclass
+  plus < term
 
+axclass
+  minus < term
+
+axclass
+  times < term
+
+consts
   "+"           :: ['a::plus, 'a] => 'a             (infixl 65)
   "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
   "*"           :: ['a::times, 'a] => 'a            (infixl 70)
 
 
+
+(** Additional concrete syntax **)
+
 types
   letbinds  letbind
   case_syn  cases_syn
@@ -72,7 +80,7 @@
 
   "~="          :: ['a, 'a] => bool                 (infixl 50)
 
-  "@Eps"        :: [pttrn,bool] => 'a               ("(3@ _./ _)" 10)
+  "@Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" 10)
 
   (* Alternative Quantifiers *)
 
@@ -96,13 +104,34 @@
 
 translations
   "x ~= y"      == "~ (x = y)"
-  "@ x.b"       == "Eps(%x.b)"
+  "@ x.b"       == "Eps (%x. b)"
   "ALL xs. P"   => "! xs. P"
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
 
+
+syntax (symbols)
+  not           :: bool => bool                     ("\\<not> _" [40] 40)
+  "op &"        :: [bool, bool] => bool             (infixr "\\<and>" 35)
+  "op |"        :: [bool, bool] => bool             (infixr "\\<or>" 30)
+  "op -->"      :: [bool, bool] => bool             (infixr "\\<midarrow>\\<rightarrow>" 25)
+  "op o"        :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl "\\<circ>" 55)
+  "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
+  "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" 10)
+  "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
+  "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
+  "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
+  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
+  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
+  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
+  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
+
+
+
+(** Rules and definitions **)
+
 rules
 
   eq_reflection "(x=y) ==> (x==y)"
@@ -147,6 +176,7 @@
 
 end
 
+
 ML
 
 (** Choice between the HOL and Isabelle style of quantifiers **)
@@ -168,6 +198,3 @@
 
 (* start 8bit 2 *)
 (* end 8bit 2 *)
-
-
-
diff -r e6d738f2b9a9 -r b59781f2b809 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Wed Nov 27 16:48:19 1996 +0100
+++ b/src/HOL/Prod.thy	Wed Nov 27 16:51:15 1996 +0100
@@ -9,7 +9,8 @@
 
 Prod = Fun + equalities +
 
-(** Products **)
+
+(** products **)
 
 (* type definition *)
 
@@ -21,6 +22,9 @@
   ('a, 'b) "*"          (infixr 20)
     = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
 
+syntax (symbols)
+  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
+
 
 (* abstract constants and syntax *)
 
@@ -32,30 +36,37 @@
   Pair          :: "['a, 'b] => 'a * 'b"
   Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
 
-(** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
+
+(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
+
 types pttrns
 
 syntax
-  "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
+  "@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    ("_,/_")
 
-  "@Sigma"  :: "[idt,'a set,'b set] => ('a * 'b)set"
-               ("(3SIGMA _:_./ _)" 10)
-  "@Times"  :: "['a set, 'a => 'b set] => ('a * 'b) set"
-               ("_ Times _" [81,80] 80)
+  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3SIGMA _:_./ _)" 10)
+  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
 
 translations
   "(x, y, z)"   == "(x, (y, z))"
   "(x, y)"      == "Pair x y"
 
-  "%(x,y,zs).b"   == "split(%x (y,zs).b)"
-  "%(x,y).b"      == "split(%x y.b)"
+  "%(x,y,zs).b" == "split(%x (y,zs).b)"
+  "%(x,y).b"    == "split(%x y.b)"
+
+  "SIGMA x:A.B" => "Sigma A (%x.B)"
+  "A Times B"   => "Sigma A (_K B)"
 
-  "SIGMA x:A. B"  =>  "Sigma A (%x.B)"
-  "A Times B"     =>  "Sigma A (_K B)"
+syntax (symbols)
+  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
+  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
+
+
+(* definitions *)
 
 defs
   Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
@@ -65,7 +76,9 @@
   prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
   Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
 
-(** Unit **)
+
+
+(** unit **)
 
 typedef (Unit)
   unit = "{p. p = True}"