src/HOL/Hoare/Arith2.thy
changeset 8791 50b650d19641
parent 5183 89f162de39cf
child 17278 f27456a2a975
--- a/src/HOL/Hoare/Arith2.thy	Thu May 04 15:14:56 2000 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Thu May 04 15:15:37 2000 +0200
@@ -6,7 +6,7 @@
 More arithmetic.  Much of this duplicates ex/Primes.
 *)
 
-Arith2 = Power +
+Arith2 = Main +
 
 constdefs
   cd      :: [nat, nat, nat] => bool