# HG changeset patch
# User wenzelm
# Date 1444506187 -7200
# Node ID 2332d9be352b0c33abce4959dde3ab5ac835ea8f
# Parent  a705f42b244d6ac4c4fc371ff364dea3098e09d6
tuned syntax -- more symbols;

diff -r a705f42b244d -r 2332d9be352b src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/Arith.thy	Sat Oct 10 21:43:07 2015 +0200
@@ -13,31 +13,27 @@
 
 definition
   add :: "[i,i]\<Rightarrow>i"   (infixr "#+" 65) where
-  "a#+b == rec(a, b, \<lambda>u v. succ(v))"
+  "a#+b \<equiv> rec(a, b, \<lambda>u v. succ(v))"
 
 definition
   diff :: "[i,i]\<Rightarrow>i"   (infixr "-" 65) where
-  "a-b == rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))"
+  "a-b \<equiv> rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))"
 
 definition
   absdiff :: "[i,i]\<Rightarrow>i"   (infixr "|-|" 65) where
-  "a|-|b == (a-b) #+ (b-a)"
+  "a|-|b \<equiv> (a-b) #+ (b-a)"
 
 definition
   mult :: "[i,i]\<Rightarrow>i"   (infixr "#*" 70) where
-  "a#*b == rec(a, 0, \<lambda>u v. b #+ v)"
+  "a#*b \<equiv> rec(a, 0, \<lambda>u v. b #+ v)"
 
 definition
   mod :: "[i,i]\<Rightarrow>i"   (infixr "mod" 70) where
-  "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
+  "a mod b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(v) |-| b, 0, \<lambda>x y. succ(v)))"
 
 definition
   div :: "[i,i]\<Rightarrow>i"   (infixr "div" 70) where
-  "a div b == rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))"
-
-
-notation (xsymbols)
-  mult  (infixr "#\<times>" 70)
+  "a div b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))"
 
 
 lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
@@ -264,12 +260,12 @@
   An example of induction over a quantified formula (a product).
   Uses rewriting with a quantified, implicative inductive hypothesis.*)
 schematic_goal add_diff_inverse_lemma:
-  "b:N \<Longrightarrow> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
+  "b:N \<Longrightarrow> ?a : \<Prod>x:N. Eq(N, b-x, 0) \<longrightarrow> Eq(N, b #+ (x-b), x)"
 apply (NE b)
 (*strip one "universal quantifier" but not the "implication"*)
 apply (rule_tac [3] intr_rls)
 (*case analysis on x in
-    (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
+    (succ(u) <= x) \<longrightarrow> (succ(u)#+(x-succ(u)) = x) *)
 prefer 4
 apply (NE x)
 apply assumption
@@ -334,7 +330,7 @@
 done
 
 (*If a+b=0 then a=0.   Surprisingly tedious*)
-schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
+schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : \<Prod>u: Eq(N,a#+b,0) .  Eq(N,a,0)"
 apply (NE a)
 apply (rule_tac [3] replace_type)
 apply arith_rew
@@ -355,7 +351,7 @@
 
 (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
 schematic_goal absdiff_eq0_lem:
-  "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
+  "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : \<Sum>v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
 apply (unfold absdiff_def)
 apply intr
 apply eqintr
@@ -446,7 +442,7 @@
 
 (*for case analysis on whether a number is 0 or a successor*)
 lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) :
-                      Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
+                      Eq(N,a,0) + (\<Sum>x:N. Eq(N,a, succ(x)))"
 apply (NE a)
 apply (rule_tac [3] PlusI_inr)
 apply (rule_tac [2] PlusI_inl)
diff -r a705f42b244d -r 2332d9be352b src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/Bool.thy	Sat Oct 10 21:43:07 2015 +0200
@@ -11,19 +11,19 @@
 
 definition
   Bool :: "t" where
-  "Bool == T+T"
+  "Bool \<equiv> T+T"
 
 definition
   true :: "i" where
-  "true == inl(tt)"
+  "true \<equiv> inl(tt)"
 
 definition
   false :: "i" where
-  "false == inr(tt)"
+  "false \<equiv> inr(tt)"
 
 definition
   cond :: "[i,i,i]\<Rightarrow>i" where
-  "cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)"
+  "cond(a,b,c) \<equiv> when(a, \<lambda>u. b, \<lambda>u. c)"
 
 lemmas bool_defs = Bool_def true_def false_def cond_def
 
diff -r a705f42b244d -r 2332d9be352b src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/CTT.thy	Sat Oct 10 21:43:07 2015 +0200
@@ -51,7 +51,7 @@
   (*Types*)
 
   (*Functions*)
-  lambda    :: "(i \<Rightarrow> i) \<Rightarrow> i"      (binder "lam " 10)
+  lambda    :: "(i \<Rightarrow> i) \<Rightarrow> i"      (binder "\<^bold>\<lambda>" 10)
   app       :: "[i,i]\<Rightarrow>i"           (infixl "`" 60)
   (*Natural numbers*)
   Zero      :: "i"                  ("0")
@@ -59,29 +59,18 @@
   pair      :: "[i,i]\<Rightarrow>i"           ("(1<_,/_>)")
 
 syntax
-  "_PROD"   :: "[idt,t,t]\<Rightarrow>t"       ("(3PROD _:_./ _)" 10)
-  "_SUM"    :: "[idt,t,t]\<Rightarrow>t"       ("(3SUM _:_./ _)" 10)
+  "_PROD"   :: "[idt,t,t]\<Rightarrow>t"       ("(3\<Prod>_:_./ _)" 10)
+  "_SUM"    :: "[idt,t,t]\<Rightarrow>t"       ("(3\<Sum>_:_./ _)" 10)
 translations
-  "PROD x:A. B" == "CONST Prod(A, \<lambda>x. B)"
-  "SUM x:A. B"  == "CONST Sum(A, \<lambda>x. B)"
+  "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)"
+  "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum(A, \<lambda>x. B)"
 
 abbreviation
-  Arrow     :: "[t,t]\<Rightarrow>t"  (infixr "-->" 30) where
-  "A --> B == PROD _:A. B"
+  Arrow     :: "[t,t]\<Rightarrow>t"  (infixr "\<longrightarrow>" 30) where
+  "A \<longrightarrow> B \<equiv> \<Prod>_:A. B"
 abbreviation
-  Times     :: "[t,t]\<Rightarrow>t"  (infixr "*" 50) where
-  "A * B == SUM _:A. B"
-
-notation (xsymbols)
-  lambda  (binder "\<lambda>\<lambda>" 10) and
-  Elem  ("(_ /\<in> _)" [10,10] 5) and
-  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
-  Arrow  (infixr "\<longrightarrow>" 30) and
-  Times  (infixr "\<times>" 50)
-
-syntax (xsymbols)
-  "_PROD"   :: "[idt,t,t] \<Rightarrow> t"     ("(3\<Pi> _\<in>_./ _)"    10)
-  "_SUM"    :: "[idt,t,t] \<Rightarrow> t"     ("(3\<Sigma> _\<in>_./ _)" 10)
+  Times     :: "[t,t]\<Rightarrow>t"  (infixr "\<times>" 50) where
+  "A \<times> B \<equiv> \<Sum>_:A. B"
 
   (*Reduction: a weaker notion than equality;  a hack for simplification.
     Reduce[a,b] means either that  a=b:A  for some A or else that "a" and "b"
@@ -146,51 +135,51 @@
    "\<And>p a b C. \<lbrakk>p: N;  a: C(0); \<And>u v. \<lbrakk>u: N; v: C(u)\<rbrakk> \<Longrightarrow> b(u,v): C(succ(u))\<rbrakk> \<Longrightarrow>
    rec(succ(p), a, \<lambda>u v. b(u,v)) = b(p, rec(p, a, \<lambda>u v. b(u,v))) : C(succ(p))" and
 
-  (*The fourth Peano axiom.  See page 91 of Martin-Lof's book*)
+  (*The fourth Peano axiom.  See page 91 of Martin-Löf's book*)
   zero_ne_succ: "\<And>a. \<lbrakk>a: N; 0 = succ(a) : N\<rbrakk> \<Longrightarrow> 0: F" and
 
 
   (*The Product of a family of types*)
 
-  ProdF: "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> PROD x:A. B(x) type" and
+  ProdF: "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) type" and
 
   ProdFL:
-    "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> PROD x:A. B(x) = PROD x:C. D(x)" and
+    "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) = \<Prod>x:C. D(x)" and
 
   ProdI:
-    "\<And>b A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> b(x):B(x)\<rbrakk> \<Longrightarrow> lam x. b(x) : PROD x:A. B(x)" and
+    "\<And>b A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> b(x):B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b(x) : \<Prod>x:A. B(x)" and
 
   ProdIL: "\<And>b c A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> b(x) = c(x) : B(x)\<rbrakk> \<Longrightarrow>
-    lam x. b(x) = lam x. c(x) : PROD x:A. B(x)" and
+    \<^bold>\<lambda>x. b(x) = \<^bold>\<lambda>x. c(x) : \<Prod>x:A. B(x)" and
 
-  ProdE:  "\<And>p a A B. \<lbrakk>p : PROD x:A. B(x); a : A\<rbrakk> \<Longrightarrow> p`a : B(a)" and
-  ProdEL: "\<And>p q a b A B. \<lbrakk>p = q: PROD x:A. B(x); a = b : A\<rbrakk> \<Longrightarrow> p`a = q`b : B(a)" and
+  ProdE:  "\<And>p a A B. \<lbrakk>p : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> p`a : B(a)" and
+  ProdEL: "\<And>p q a b A B. \<lbrakk>p = q: \<Prod>x:A. B(x); a = b : A\<rbrakk> \<Longrightarrow> p`a = q`b : B(a)" and
 
-  ProdC: "\<And>a b A B. \<lbrakk>a : A; \<And>x. x:A \<Longrightarrow> b(x) : B(x)\<rbrakk> \<Longrightarrow> (lam x. b(x)) ` a = b(a) : B(a)" and
+  ProdC: "\<And>a b A B. \<lbrakk>a : A; \<And>x. x:A \<Longrightarrow> b(x) : B(x)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x)) ` a = b(a) : B(a)" and
 
-  ProdC2: "\<And>p A B. p : PROD x:A. B(x) \<Longrightarrow> (lam x. p`x) = p : PROD x:A. B(x)" and
+  ProdC2: "\<And>p A B. p : \<Prod>x:A. B(x) \<Longrightarrow> (\<^bold>\<lambda>x. p`x) = p : \<Prod>x:A. B(x)" and
 
 
   (*The Sum of a family of types*)
 
-  SumF:  "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> SUM x:A. B(x) type" and
-  SumFL: "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> SUM x:A. B(x) = SUM x:C. D(x)" and
+  SumF:  "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) type" and
+  SumFL: "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) = \<Sum>x:C. D(x)" and
 
-  SumI:  "\<And>a b A B. \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> <a,b> : SUM x:A. B(x)" and
-  SumIL: "\<And>a b c d A B. \<lbrakk> a = c : A; b = d : B(a)\<rbrakk> \<Longrightarrow> <a,b> = <c,d> : SUM x:A. B(x)" and
+  SumI:  "\<And>a b A B. \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> <a,b> : \<Sum>x:A. B(x)" and
+  SumIL: "\<And>a b c d A B. \<lbrakk> a = c : A; b = d : B(a)\<rbrakk> \<Longrightarrow> <a,b> = <c,d> : \<Sum>x:A. B(x)" and
 
-  SumE: "\<And>p c A B C. \<lbrakk>p: SUM x:A. B(x); \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y): C(<x,y>)\<rbrakk>
+  SumE: "\<And>p c A B C. \<lbrakk>p: \<Sum>x:A. B(x); \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y): C(<x,y>)\<rbrakk>
     \<Longrightarrow> split(p, \<lambda>x y. c(x,y)) : C(p)" and
 
-  SumEL: "\<And>p q c d A B C. \<lbrakk>p = q : SUM x:A. B(x);
+  SumEL: "\<And>p q c d A B C. \<lbrakk>p = q : \<Sum>x:A. B(x);
       \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y)=d(x,y): C(<x,y>)\<rbrakk>
     \<Longrightarrow> split(p, \<lambda>x y. c(x,y)) = split(q, \<lambda>x y. d(x,y)) : C(p)" and
 
   SumC: "\<And>a b c A B C. \<lbrakk>a: A;  b: B(a); \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y): C(<x,y>)\<rbrakk>
     \<Longrightarrow> split(<a,b>, \<lambda>x y. c(x,y)) = c(a,b) : C(<a,b>)" and
 
-  fst_def:   "\<And>a. fst(a) == split(a, \<lambda>x y. x)" and
-  snd_def:   "\<And>a. snd(a) == split(a, \<lambda>x y. y)" and
+  fst_def:   "\<And>a. fst(a) \<equiv> split(a, \<lambda>x y. x)" and
+  snd_def:   "\<And>a. snd(a) \<equiv> split(a, \<lambda>x y. y)" and
 
 
   (*The sum of two types*)
@@ -245,7 +234,7 @@
   FEL: "\<And>p q C. \<lbrakk>p = q : F; C type\<rbrakk> \<Longrightarrow> contr(p) = contr(q) : C" and
 
   (*The type T
-     Martin-Lof's book (page 68) discusses elimination and computation.
+     Martin-Löf's book (page 68) discusses elimination and computation.
      Elimination can be derived by computation and equality of types,
      but with an extra premise C(x) type x:T.
      Also computation can be derived from elimination. *)
@@ -428,7 +417,7 @@
 fun add_mp_tac ctxt i =
   resolve_tac ctxt @{thms subst_prodE} i  THEN  assume_tac ctxt i  THEN  assume_tac ctxt i
 
-(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
+(*Finds P\<longrightarrow>Q and P in the assumptions, replaces implication by Q *)
 fun mp_tac ctxt i = eresolve_tac ctxt @{thms subst_prodE} i  THEN  assume_tac ctxt i
 
 (*"safe" when regarded as predicate calculus rules*)
diff -r a705f42b244d -r 2332d9be352b src/CTT/ex/Elimination.thy
--- a/src/CTT/ex/Elimination.thy	Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/ex/Elimination.thy	Sat Oct 10 21:43:07 2015 +0200
@@ -14,36 +14,36 @@
 
 text "This finds the functions fst and snd!"
 
-schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
+schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
 apply pc
 done
 
-schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
+schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
 apply pc
 back
 done
 
 text "Double negation of the Excluded Middle"
-schematic_goal "A type \<Longrightarrow> ?a : ((A + (A-->F)) --> F) --> F"
+schematic_goal "A type \<Longrightarrow> ?a : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"
 apply intr
 apply (rule ProdE)
 apply assumption
 apply pc
 done
 
-schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A*B) \<longrightarrow> (B*A)"
+schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B) \<longrightarrow> (B \<times> A)"
 apply pc
 done
 (*The sequent version (ITT) could produce an interesting alternative
   by backtracking.  No longer.*)
 
 text "Binary sums and products"
-schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A + B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> C) \<times> (B \<longrightarrow> C)"
 apply pc
 done
 
 (*A distributive law*)
-schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A * (B+C)  -->  (A*B + A*C)"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A \<times> (B + C) \<longrightarrow> (A \<times> B + A \<times> C)"
 apply pc
 done
 
@@ -52,12 +52,12 @@
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     and "\<And>x. x:A \<Longrightarrow> C(x) type"
-  shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
+  shows "?a : (\<Sum>x:A. B(x) + C(x)) \<longrightarrow> (\<Sum>x:A. B(x)) + (\<Sum>x:A. C(x))"
 apply (pc assms)
 done
 
 text "Construction of the currying functional"
-schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A*B --> C) --> (A--> (B-->C))"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))"
 apply pc
 done
 
@@ -65,14 +65,14 @@
 schematic_goal
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
-    and "\<And>z. z: (SUM x:A. B(x)) \<Longrightarrow> C(z) type"
-  shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
-                      (PROD x:A . PROD y:B(x) . C(<x,y>))"
+    and "\<And>z. z: (\<Sum>x:A. B(x)) \<Longrightarrow> C(z) type"
+  shows "?a : \<Prod>f: (\<Prod>z : (\<Sum>x:A . B(x)) . C(z)).
+                      (\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))"
 apply (pc assms)
 done
 
-text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
-schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> (B-->C)) --> (A*B --> C)"
+text "Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<times> B \<longrightarrow> C)"
 apply pc
 done
 
@@ -80,14 +80,14 @@
 schematic_goal
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
-    and "\<And>z. z: (SUM x:A . B(x)) \<Longrightarrow> C(z) type"
-  shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
-        --> (PROD z : (SUM x:A . B(x)) . C(z))"
+    and "\<And>z. z: (\<Sum>x:A . B(x)) \<Longrightarrow> C(z) type"
+  shows "?a : (\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))
+        \<longrightarrow> (\<Prod>z : (\<Sum>x:A . B(x)) . C(z))"
 apply (pc assms)
 done
 
 text "Function application"
-schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A --> B) * A) --> B"
+schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A \<longrightarrow> B) \<times> A) \<longrightarrow> B"
 apply pc
 done
 
@@ -97,46 +97,46 @@
     and "B type"
     and "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> C(x,y) type"
   shows
-    "?a :     (SUM y:B . PROD x:A . C(x,y))
-          --> (PROD x:A . SUM y:B . C(x,y))"
+    "?a :     (\<Sum>y:B . \<Prod>x:A . C(x,y))
+          \<longrightarrow> (\<Prod>x:A . \<Sum>y:B . C(x,y))"
 apply (pc assms)
 done
 
-text "Martin-Lof (1984) pages 36-7: the combinator S"
+text "Martin-Löf (1984) pages 36-7: the combinator S"
 schematic_goal
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
-  shows "?a :    (PROD x:A. PROD y:B(x). C(x,y))
-             --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+  shows "?a :    (\<Prod>x:A. \<Prod>y:B(x). C(x,y))
+             \<longrightarrow> (\<Prod>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
 apply (pc assms)
 done
 
-text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
+text "Martin-Löf (1984) page 58: the axiom of disjunction elimination"
 schematic_goal
   assumes "A type"
     and "B type"
     and "\<And>z. z: A+B \<Longrightarrow> C(z) type"
-  shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
-          --> (PROD z: A+B. C(z))"
+  shows "?a : (\<Prod>x:A. C(inl(x))) \<longrightarrow> (\<Prod>y:B. C(inr(y)))
+          \<longrightarrow> (\<Prod>z: A+B. C(z))"
 apply (pc assms)
 done
 
 (*towards AXIOM OF CHOICE*)
 schematic_goal [folded basic_defs]:
-  "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
+  "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> B \<times> C) \<longrightarrow> (A \<longrightarrow> B) \<times> (A \<longrightarrow> C)"
 apply pc
 done
 
 
-(*Martin-Lof (1984) page 50*)
+(*Martin-Löf (1984) page 50*)
 text "AXIOM OF CHOICE!  Delicate use of elimination rules"
 schematic_goal
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
-  shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
-                         (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+  shows "?a : \<Prod>h: (\<Prod>x:A. \<Sum>y:B(x). C(x,y)).
+                         (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
 apply (intr assms)
 prefer 2 apply add_mp
 prefer 2 apply add_mp
@@ -153,8 +153,8 @@
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
-  shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
-                         (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+  shows "?a : \<Prod>h: (\<Prod>x:A. \<Sum>y:B(x). C(x,y)).
+                         (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
 apply (intr assms)
 (*Must not use add_mp as subst_prodE hides the construction.*)
 apply (rule ProdE [THEN SumE])
@@ -174,13 +174,13 @@
 done
 
 text "Example of sequent_style deduction"
-(*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
-    lam u. split(u,\<lambda>v w.split(v,\<lambda>x y.lam z. <x,<y,z>>) ` w)     *)
+(*When splitting z:A \<times> B, the assumption C(z) is affected;  ?a becomes
+    \<^bold>\<lambda>u. split(u,\<lambda>v w.split(v,\<lambda>x y.\<^bold> \<lambda>z. <x,<y,z>>) ` w)     *)
 schematic_goal
   assumes "A type"
     and "B type"
-    and "\<And>z. z:A*B \<Longrightarrow> C(z) type"
-  shows "?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))"
+    and "\<And>z. z:A \<times> B \<Longrightarrow> C(z) type"
+  shows "?a : (\<Sum>z:A \<times> B. C(z)) \<longrightarrow> (\<Sum>u:A. \<Sum>v:B. C(<u,v>))"
 apply (rule intr_rls)
 apply (tactic \<open>biresolve_tac @{context} safe_brls 2\<close>)
 (*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
diff -r a705f42b244d -r 2332d9be352b src/CTT/ex/Equality.thy
--- a/src/CTT/ex/Equality.thy	Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/ex/Equality.thy	Sat Oct 10 21:43:07 2015 +0200
@@ -43,20 +43,20 @@
 apply hyp_rew
 done
 
-(*Martin-Lof (1984) page 62: pairing is surjective*)
+(*Martin-Löf (1984) page 62: pairing is surjective*)
 lemma "p : Sum(A,B) \<Longrightarrow> <split(p,\<lambda>x y. x), split(p,\<lambda>x y. y)> = p : Sum(A,B)"
 apply (rule EqE)
 apply (rule elim_rls, assumption)
 apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac @{context} [])\<close>) (*!!!!!!!*)
 done
 
-lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (lam u. split(u, \<lambda>v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
+lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) ` <a,b> = <b,a> : \<Sum>x:B. A"
 apply rew
 done
 
 (*a contrived, complicated simplication, requires sum-elimination also*)
-lemma "(lam f. lam x. f`(f`x)) ` (lam u. split(u, \<lambda>v w.<w,v>)) =
-      lam x. x  :  PROD x:(SUM y:N. N). (SUM y:N. N)"
+lemma "(\<^bold>\<lambda>f. \<^bold>\<lambda>x. f`(f`x)) ` (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) =
+      \<^bold>\<lambda>x. x  :  \<Prod>x:(\<Sum>y:N. N). (\<Sum>y:N. N)"
 apply (rule reduction_rls)
 apply (rule_tac [3] intrL_rls)
 apply (rule_tac [4] EqE)
diff -r a705f42b244d -r 2332d9be352b src/CTT/ex/Synthesis.thy
--- a/src/CTT/ex/Synthesis.thy	Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/ex/Synthesis.thy	Sat Oct 10 21:43:07 2015 +0200
@@ -10,8 +10,7 @@
 begin
 
 text "discovery of predecessor function"
-schematic_goal "?a : SUM pred:?A . Eq(N, pred`0, 0)
-                  *  (PROD n:N. Eq(N, pred ` succ(n), n))"
+schematic_goal "?a : \<Sum>pred:?A . Eq(N, pred`0, 0) \<times> (\<Prod>n:N. Eq(N, pred ` succ(n), n))"
 apply intr
 apply eqintr
 apply (rule_tac [3] reduction_rls)
@@ -21,7 +20,7 @@
 
 text "the function fst as an element of a function type"
 schematic_goal [folded basic_defs]:
-  "A type \<Longrightarrow> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
+  "A type \<Longrightarrow> ?a: \<Sum>f:?B . \<Prod>i:A. \<Prod>j:A. Eq(A, f ` <i,j>, i)"
 apply intr
 apply eqintr
 apply (rule_tac [2] reduction_rls)
@@ -34,8 +33,8 @@
 text "An interesting use of the eliminator, when"
 (*The early implementation of unification caused non-rigid path in occur check
   See following example.*)
-schematic_goal "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
-                   * Eq(?A, ?b(inr(i)), <succ(0), i>)"
+schematic_goal "?a : \<Prod>i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
+                   \<times> Eq(?A, ?b(inr(i)), <succ(0), i>)"
 apply intr
 apply eqintr
 apply (rule comp_rls)
@@ -45,16 +44,16 @@
 (*Here we allow the type to depend on i.
  This prevents the cycle in the first unification (no longer needed).
  Requires flex-flex to preserve the dependence.
- Simpler still: make ?A into a constant type N*N.*)
-schematic_goal "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
-                  *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
+ Simpler still: make ?A into a constant type N \<times> N.*)
+schematic_goal "?a : \<Prod>i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
+                  \<times>  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
 oops
 
 text "A tricky combination of when and split"
 (*Now handled easily, but caused great problems once*)
 schematic_goal [folded basic_defs]:
-  "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
-                           *  Eq(?A, ?b(inr(<i,j>)), j)"
+  "?a : \<Prod>i:N. \<Prod>j:N. Eq(?A, ?b(inl(<i,j>)), i)
+                           \<times>  Eq(?A, ?b(inr(<i,j>)), j)"
 apply intr
 apply eqintr
 apply (rule PlusC_inl [THEN trans_elem])
@@ -65,20 +64,20 @@
 done
 
 (*similar but allows the type to depend on i and j*)
-schematic_goal "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
-                          *   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
+schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
+                          \<times>   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
 oops
 
 (*similar but specifying the type N simplifies the unification problems*)
-schematic_goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
-                          *   Eq(N, ?b(inr(<i,j>)), j)"
+schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(N, ?b(inl(<i,j>)), i)
+                          \<times>   Eq(N, ?b(inr(<i,j>)), j)"
 oops
 
 
 text "Deriving the addition operator"
 schematic_goal [folded arith_defs]:
-  "?c : PROD n:N. Eq(N, ?f(0,n), n)
-                  *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
+  "?c : \<Prod>n:N. Eq(N, ?f(0,n), n)
+                  \<times>  (\<Prod>m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
 apply intr
 apply eqintr
 apply (rule comp_rls)
@@ -87,9 +86,9 @@
 
 text "The addition function -- using explicit lambdas"
 schematic_goal [folded arith_defs]:
-  "?c : SUM plus : ?A .
-         PROD x:N. Eq(N, plus`0`x, x)
-                *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
+  "?c : \<Sum>plus : ?A .
+         \<Prod>x:N. Eq(N, plus`0`x, x)
+                \<times>  (\<Prod>y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
 apply intr
 apply eqintr
 apply (tactic "resolve_tac @{context} [TSimp.split_eqn] 3")
diff -r a705f42b244d -r 2332d9be352b src/CTT/ex/Typechecking.thy
--- a/src/CTT/ex/Typechecking.thy	Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/ex/Typechecking.thy	Sat Oct 10 21:43:07 2015 +0200
@@ -22,7 +22,7 @@
 apply (rule form_rls)
 done
 
-schematic_goal "PROD z:?A . N + ?B(z) type"
+schematic_goal "\<Prod>z:?A . N + ?B(z) type"
 apply (rule form_rls)
 apply (rule form_rls)
 apply (rule form_rls)
@@ -33,7 +33,7 @@
 
 subsection \<open>Multi-step proofs: Type inference\<close>
 
-lemma "PROD w:N. N + N type"
+lemma "\<Prod>w:N. N + N type"
 apply form
 done
 
@@ -41,26 +41,26 @@
 apply intr
 done
 
-schematic_goal "PROD w:N . Eq(?A,w,w) type"
+schematic_goal "\<Prod>w:N . Eq(?A,w,w) type"
 apply typechk
 done
 
-schematic_goal "PROD x:N . PROD y:N . Eq(?A,x,y) type"
+schematic_goal "\<Prod>x:N . \<Prod>y:N . Eq(?A,x,y) type"
 apply typechk
 done
 
 text "typechecking an application of fst"
-schematic_goal "(lam u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
+schematic_goal "(\<^bold>\<lambda>u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
 apply typechk
 done
 
 text "typechecking the predecessor function"
-schematic_goal "lam n. rec(n, 0, \<lambda>x y. x) : ?A"
+schematic_goal "\<^bold>\<lambda>n. rec(n, 0, \<lambda>x y. x) : ?A"
 apply typechk
 done
 
 text "typechecking the addition function"
-schematic_goal "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
+schematic_goal "\<^bold>\<lambda>n. \<^bold>\<lambda>m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
 apply typechk
 done
 
@@ -69,18 +69,18 @@
 method_setup N =
   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close>
 
-schematic_goal "lam w. <w,w> : ?A"
+schematic_goal "\<^bold>\<lambda>w. <w,w> : ?A"
 apply typechk
 apply N
 done
 
-schematic_goal "lam x. lam y. x : ?A"
+schematic_goal "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : ?A"
 apply typechk
 apply N
 done
 
 text "typechecking fst (as a function object)"
-schematic_goal "lam i. split(i, \<lambda>j k. j) : ?A"
+schematic_goal "\<^bold>\<lambda>i. split(i, \<lambda>j k. j) : ?A"
 apply typechk
 apply N
 done