src/HOL/PreList.thy
author paulson
Fri, 21 Apr 2000 11:28:18 +0200
changeset 8756 b03a0b219139
parent 8563 2746bc9a7ef2
child 8840 18b76c137c41
permissions -rw-r--r--
new file Integ/NatSimprocs.ML
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 =
8563
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
    11
  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation
8756
b03a0b219139 new file Integ/NatSimprocs.ML
paulson
parents: 8563
diff changeset
    12
  + SVC_Oracle
b03a0b219139 new file Integ/NatSimprocs.ML
paulson
parents: 8563
diff changeset
    13
files "Integ/NatSimprocs.ML":
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    14
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    15
end