src/Cube/LP2.thy
author paulson
Wed, 25 Nov 1998 15:54:41 +0100
changeset 5971 c5a7a7685826
parent 4583 6d9be46ea566
permissions -rw-r--r--
simplified ensures_UNIV
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4583
6d9be46ea566 reorganized into individual theories;
wenzelm
parents:
diff changeset
     1
6d9be46ea566 reorganized into individual theories;
wenzelm
parents:
diff changeset
     2
LP2 = LP + L2