src/ZF/Main.thy
author nipkow
Tue, 17 Oct 2000 08:00:46 +0200
changeset 10228 e653cb933293
parent 9578 ab26d6c8ebfe
child 12426 9032bdbc2125
permissions -rw-r--r--
added intermediate value thms
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5157
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     1
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     2
(*$Id$
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     3
  theory Main includes everything*)
6e03de8ec2b4 as in HOL
paulson
parents:
diff changeset
     4
9578
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents: 9570
diff changeset
     5
Main = Update + InfDatatype + List + EquivClass + IntDiv
9175
6f8499d86d4f finally theory Bin (the integers) is included
paulson
parents: 5531
diff changeset
     6