src/HOL/Main.thy
author paulson
Fri, 07 Jan 2000 11:00:56 +0100
changeset 8112 efbe50e2bef9
parent 7143 9c02848c5404
child 8490 6e0f23304061
permissions -rw-r--r--
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5123
97c1d5c7b701 stepping stones;
wenzelm
parents:
diff changeset
     1
5126
01cbf154d926 theory Main includes everything;
wenzelm
parents: 5123
diff changeset
     2
(*theory Main includes everything*)
01cbf154d926 theory Main includes everything;
wenzelm
parents: 5123
diff changeset
     3
7143
9c02848c5404 the SVC link-up
paulson
parents: 7038
diff changeset
     4
Main = NatBin + Map + Recdef + Record + RelPow + Sexp + String + Calculation +
9c02848c5404 the SVC link-up
paulson
parents: 7038
diff changeset
     5
       SVC_Oracle