src/HOL/PreList.thy
author wenzelm
Thu, 17 Aug 2000 10:33:37 +0200
changeset 9619 6125cc9efc18
parent 9066 b1e874e38dab
child 10212 33fe2d701ddd
permissions -rw-r--r--
fixed deps;
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 + 
9619
6125cc9efc18 fixed deps;
wenzelm
parents: 9066
diff changeset
    12
  SVC_Oracle + While:
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    13
9066
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8862
diff changeset
    14
theorems [cases type: bool] = case_split
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8862
diff changeset
    15
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    16
end