src/HOL/PreList.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8862 78643f8449c6
child 9066 b1e874e38dab
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8563
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     1
(*  Title:      HOL/List.thy
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     2
    ID:         $Id$
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     3
    Author:     Tobias Nipkow
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     4
    Copyright   2000 TU Muenchen
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     5
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     6
A basis for building theory List on. Is defined separately to serve as a
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     7
basis for theory ToyList in the documentation.
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     8
*)
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
     9
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    10
theory PreList =
8862
78643f8449c6 NatSimprocs is now a theory, not a file
paulson
parents: 8840
diff changeset
    11
  Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
78643f8449c6 NatSimprocs is now a theory, not a file
paulson
parents: 8840
diff changeset
    12
  SVC_Oracle:
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    13
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    14
end