src/ZF/Inductive.thy
author lcp
Fri, 16 Dec 1994 17:38:14 +0100
changeset 798 31ec33d96231
parent 578 efc648d29dd0
child 805 96f51689cdeb
permissions -rw-r--r--
added thy_syntax.ML

(*Dummy theory to document dependencies *)

Inductive = "indrule"