src/Cube/LPomega.thy
author nipkow
Wed, 24 Jun 1998 13:59:45 +0200
changeset 5077 71043526295f
parent 4583 6d9be46ea566
permissions -rw-r--r--
* HOL/List: new function list_update written xs[i:=v] that updates the i-th list position. May also be iterated as in xs[i:=a,j:=b,...].
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
LPomega = LP + Lomega