src/HOL/Recdef.thy
author wenzelm
Fri, 16 Apr 1999 14:49:06 +0200
changeset 6438 e55a1869ed38
parent 5123 97c1d5c7b701
child 7357 d0e16da40ea2
permissions -rw-r--r--
'HOL/recdef' theory data; induct method setup;
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