# HG changeset patch
# User wenzelm
# Date 1149265488 -7200
# Node ID 957bcf55c98f2962c029aec75c1d8ee31b5303b0
# Parent  5cd82054c2c696037a40c95dcd27983c97543610
tuned;

diff -r 5cd82054c2c6 -r 957bcf55c98f src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Fri Jun 02 18:15:38 2006 +0200
+++ b/src/CTT/Arith.thy	Fri Jun 02 18:24:48 2006 +0200
@@ -12,27 +12,32 @@
 
 subsection {* Arithmetic operators and their definitions *}
 
-consts
-  "#+"  :: "[i,i]=>i"   (infixr 65)
-  "-"   :: "[i,i]=>i"   (infixr 65)
-  "|-|" :: "[i,i]=>i"   (infixr 65)
-  "#*"  :: "[i,i]=>i"   (infixr 70)
-  div   :: "[i,i]=>i"   (infixr 70)
-  mod   :: "[i,i]=>i"   (infixr 70)
+definition
+  add :: "[i,i]=>i"   (infixr "#+" 65)
+  "a#+b == rec(a, b, %u v. succ(v))"
 
-syntax (xsymbols)
-  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
+  diff :: "[i,i]=>i"   (infixr "-" 65)
+  "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
+
+  absdiff :: "[i,i]=>i"   (infixr "|-|" 65)
+  "a|-|b == (a-b) #+ (b-a)"
+
+  mult :: "[i,i]=>i"   (infixr "#*" 70)
+  "a#*b == rec(a, 0, %u v. b #+ v)"
 
-syntax (HTML output)
-  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
+  mod :: "[i,i]=>i"   (infixr "mod" 70)
+  "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
+
+  div :: "[i,i]=>i"   (infixr "div" 70)
+  "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
+
 
-defs
-  add_def:     "a#+b == rec(a, b, %u v. succ(v))"
-  diff_def:    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
-  absdiff_def: "a|-|b == (a-b) #+ (b-a)"
-  mult_def:    "a#*b == rec(a, 0, %u v. b #+ v)"
-  mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
-  div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
+const_syntax (xsymbols)
+  mult  (infixr "#\<times>" 70)
+
+const_syntax (HTML output)
+  mult (infixr "#\<times>" 70)
+
 
 lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
 
diff -r 5cd82054c2c6 -r 957bcf55c98f src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Fri Jun 02 18:15:38 2006 +0200
+++ b/src/CTT/Bool.thy	Fri Jun 02 18:24:48 2006 +0200
@@ -10,7 +10,7 @@
 imports CTT
 begin
 
-constdefs
+definition
   Bool :: "t"
   "Bool == T+T"
 
diff -r 5cd82054c2c6 -r 957bcf55c98f src/CTT/README.html
--- a/src/CTT/README.html	Fri Jun 02 18:15:38 2006 +0200
+++ b/src/CTT/README.html	Fri Jun 02 18:24:48 2006 +0200
@@ -18,8 +18,8 @@
 Useful references on Constructive Type Theory:
 
 <UL>
-<LI>	B. Nordstrm, K. Petersson and J. M. Smith,<BR>
-	Programming in Martin-Lf's Type Theory<BR>
+<LI>	B. Nordström, K. Petersson and J. M. Smith,<BR>
+	Programming in Martin-Löf's Type Theory<BR>
 	(Oxford University Press, 1990)
 
 <LI>	Simon Thompson,<BR>