# HG changeset patch
# User berghofe
# Date 1170865609 -3600
# Node ID 9e185f78e7d42d0430ac86dc6e4eae53bce94e9e
# Parent  45f01828cb69830549535b9272321c4f5958eefa
Adapted to changes in Transitive_Closure theory.

diff -r 45f01828cb69 -r 9e185f78e7d4 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Feb 07 17:26:04 2007 +0100
+++ b/src/HOL/Divides.thy	Wed Feb 07 17:26:49 2007 +0100
@@ -32,9 +32,9 @@
   mod (infixl "mod" 70)
 
 instance nat :: "Divides.div"
-  mod_def: "m mod n == wfrec (trancl pred_nat)
+  mod_def: "m mod n == wfrec (pred_nat^+)
                           (%f j. if j<n | n=0 then j else f (j-n)) m"
-  div_def:   "m div n == wfrec (trancl pred_nat) 
+  div_def:   "m div n == wfrec (pred_nat^+) 
                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
 
 definition
@@ -61,10 +61,10 @@
                   standard]
 
 lemma mod_eq: "(%m. m mod n) = 
-              wfrec (trancl pred_nat) (%f j. if j<n | n=0 then j else f (j-n))"
+              wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
 by (simp add: mod_def)
 
-lemma div_eq: "(%m. m div n) = wfrec (trancl pred_nat)  
+lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)  
                (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
 by (simp add: div_def)
 
diff -r 45f01828cb69 -r 9e185f78e7d4 src/HOL/Wellfounded_Relations.thy
--- a/src/HOL/Wellfounded_Relations.thy	Wed Feb 07 17:26:04 2007 +0100
+++ b/src/HOL/Wellfounded_Relations.thy	Wed Feb 07 17:26:49 2007 +0100
@@ -16,7 +16,7 @@
 
 constdefs
  less_than :: "(nat*nat)set"
-    "less_than == trancl pred_nat"
+    "less_than == pred_nat^+"
 
  measure   :: "('a => nat) => ('a * 'a)set"
     "measure == inv_image less_than"