src/HOL/Recdef.thy
author paulson
Thu, 10 Jun 1999 10:39:38 +0200
changeset 6811 4700ca722bbd
parent 6438 e55a1869ed38
child 7357 d0e16da40ea2
permissions -rw-r--r--
Always_LeadsTo_pre. Always_LeadsTo_post: new equivalences suggested by Misra
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5123
97c1d5c7b701 stepping stones;
wenzelm
parents:
diff changeset
     1
6438
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
     2
Recdef = WF_Rel +
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
     3
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
     4
setup RecdefPackage.setup
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
     5
setup InductMethod.setup
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
     6
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
     7
end