src/HOL/Recdef.thy
author berghofe
Fri, 23 Oct 1998 22:36:15 +0200
changeset 5760 7e2cf2820684
parent 5123 97c1d5c7b701
child 6438 e55a1869ed38
permissions -rw-r--r--
Added theorems True_not_False and False_not_True (for rep_datatype).


Recdef = WF_Rel