Theorem provers allow mechanic verification of formal proofs of mathematical theorems. An important feature for formalizing recursive structures such as programming language semantics are inductively defined predicates. The currently existing provers allow inductive specification of predicates with a fixed set of introduction rules. This thesis explores the idea of open inductive predicates which allow addition of introduction rules after definition and proofs for theorems on a per-introduction-rule basis. It also presents an implementation of the concept for the Isabelle theorem prover.