src/Cube/CC.thy
author paulson
Thu, 25 Jul 2002 10:56:35 +0200
changeset 13422 af9bc8d87a75
parent 4583 6d9be46ea566
permissions -rw-r--r--
Added the assumption nth_replacement to locale M_datatypes. Moved up its proof to make it available for the instantiation of that locale.


CC = L2 + LP + Lomega