src/ZF/Main.thy
author paulson
Fri, 11 Aug 2000 13:27:17 +0200
changeset 9578 ab26d6c8ebfe
parent 9570 e16e168984e1
child 12426 9032bdbc2125
permissions -rw-r--r--
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
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