src/HOL/Recdef.thy
author wenzelm
Tue, 24 Aug 1999 11:50:58 +0200
changeset 7333 6cb15c6f1d9f
parent 6438 e55a1869ed38
child 7357 d0e16da40ea2
permissions -rw-r--r--
isar: no_pos flag;
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