src/HOL/Mutabelle/Mutabelle.thy
changeset 35092 cfe605c54e50
parent 34974 18b41bba42b5
child 35267 8dfd816713c6
     1.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Wed Feb 10 14:12:04 2010 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    (@{const_name dummy_pattern}, "'a::{}"),
     1.5    (@{const_name Algebras.uminus}, "'a"),
     1.6    (@{const_name Nat.size}, "'a"),
     1.7 -  (@{const_name Algebras.abs}, "'a")];
     1.8 +  (@{const_name Groups.abs}, "'a")];
     1.9  
    1.10  val forbidden_thms =
    1.11   ["finite_intvl_succ_class",