src/ZF/indrule.thy
author nipkow
Wed, 24 Jun 1998 13:59:45 +0200
changeset 5077 71043526295f
parent 1736 fe0b459273f2
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,...].

(*Dummy theory to document dependencies *)

indrule = "ind_syntax" + "cartprod" + "intr_elim"