# HG changeset patch
# User paulson
# Date 906643290 -7200
# Node ID a48cbe410618f9f2db4565efbb0210a267764d0f
# Parent  9117a0e2bf3186be225e00b5bb375b19250dfff6
renamed some axioms

diff -r 9117a0e2bf31 -r a48cbe410618 src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Thu Sep 24 15:20:29 1998 +0200
+++ b/src/HOL/Integ/Bin.thy	Thu Sep 24 15:21:30 1998 +0200
@@ -39,7 +39,7 @@
   bin_pred         :: bin=>bin
   bin_minus        :: bin=>bin
   bin_add,bin_mult :: [bin,bin]=>bin
-  h_bin            :: [bin,bool,bin]=>bin
+  adding            :: [bin,bool,bin]=>bin
 
 (*NCons inserts a bit, suppressing leading 0s and 1s*)
 primrec
@@ -54,44 +54,44 @@
 	                             (integ_of w) + (integ_of w)" 
 
 primrec
-  succ_Pls  "bin_succ Pls = Pls BIT True" 
-  succ_Min  "bin_succ Min = Pls"
-  succ_BIT  "bin_succ(w BIT x) =
-  	        (if x then bin_succ w BIT False
-	              else NCons w True)"
+  bin_succ_Pls  "bin_succ Pls = Pls BIT True" 
+  bin_succ_Min  "bin_succ Min = Pls"
+  bin_succ_BIT  "bin_succ(w BIT x) =
+  	            (if x then bin_succ w BIT False
+	                  else NCons w True)"
 
 primrec
-  pred_Pls  "bin_pred Pls = Min"
-  pred_Min  "bin_pred Min = Min BIT False"
-  pred_BIT  "bin_pred(w BIT x) =
-	        (if x then NCons w False
-		      else (bin_pred w) BIT True)"
+  bin_pred_Pls  "bin_pred Pls = Min"
+  bin_pred_Min  "bin_pred Min = Min BIT False"
+  bin_pred_BIT  "bin_pred(w BIT x) =
+	            (if x then NCons w False
+		          else (bin_pred w) BIT True)"
  
 primrec
-  minus_Pls  "bin_minus Pls = Pls"
-  minus_Min  "bin_minus Min = Pls BIT True"
-  minus_BIT  "bin_minus(w BIT x) =
-	         (if x then bin_pred (NCons (bin_minus w) False)
-		       else bin_minus w BIT False)"
+  bin_minus_Pls  "bin_minus Pls = Pls"
+  bin_minus_Min  "bin_minus Min = Pls BIT True"
+  bin_minus_BIT  "bin_minus(w BIT x) =
+	             (if x then bin_pred (NCons (bin_minus w) False)
+		           else bin_minus w BIT False)"
 
 primrec
-  add_Pls  "bin_add Pls w = w"
-  add_Min  "bin_add Min w = bin_pred w"
-  add_BIT  "bin_add (v BIT x) w = h_bin v x w"
+  bin_add_Pls  "bin_add Pls w = w"
+  bin_add_Min  "bin_add Min w = bin_pred w"
+  bin_add_BIT  "bin_add (v BIT x) w = adding v x w"
 
 primrec
-  "h_bin v x Pls = v BIT x"
-  "h_bin v x Min = bin_pred (v BIT x)"
-  "h_bin v x (w BIT y) =
-	     NCons (bin_add v (if (x & y) then bin_succ w else w))
+  "adding v x Pls = v BIT x"
+  "adding v x Min = bin_pred (v BIT x)"
+  "adding v x (w BIT y) =
+ 	     NCons (bin_add v (if (x & y) then bin_succ w else w))
 	           (x~=y)" 
 
 primrec
-  mult_Pls  "bin_mult Pls w = Pls"
-  mult_Min  "bin_mult Min w = bin_minus w"
-  mult_BIT  "bin_mult (v BIT x) w =
-	        (if x then (bin_add (NCons (bin_mult v w) False) w)
-	              else (NCons (bin_mult v w) False))"
+  bin_mult_Pls  "bin_mult Pls w = Pls"
+  bin_mult_Min  "bin_mult Min w = bin_minus w"
+  bin_mult_BIT  "bin_mult (v BIT x) w =
+	            (if x then (bin_add (NCons (bin_mult v w) False) w)
+	                  else (NCons (bin_mult v w) False))"
 
 
 end