src/Pure/Tools/ROOT.ML
author berghofe
Tue, 13 Nov 2007 11:02:55 +0100
changeset 25425 9191942c4ead
parent 24280 c9867bdf2424
child 25525 d6b898681fc7
permissions -rw-r--r--
Removed some case_names and consumes attributes that are now no longer needed due to changes in the to_pred and to_set attributes.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
     1
(*  Title:      Pure/Tools/ROOT.ML
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
     2
    ID:         $Id$
16842
wenzelm
parents: 16781
diff changeset
     3
wenzelm
parents: 16781
diff changeset
     4
Miscellaneous tools and packages for Pure Isabelle.
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
     5
*)
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
     6
24046
10f681043e07 added Tools/named_thms.ML;
wenzelm
parents: 23614
diff changeset
     7
use "named_thms.ML";
10f681043e07 added Tools/named_thms.ML;
wenzelm
parents: 23614
diff changeset
     8
23614
4724a6b90af4 moved General/xml.ML to Tools/xml.ML;
wenzelm
parents: 23174
diff changeset
     9
(*basic XML support*)
22208
2d6e8cf48670 shifted import order
haftmann
parents: 22023
diff changeset
    10
use "xml_syntax.ML";
20708
29c1754b250f changed order
haftmann
parents: 20657
diff changeset
    11
19812
60c6bfbf6ca1 added invoke.ML;
wenzelm
parents: 19341
diff changeset
    12
(*derived theory and proof elements*)
60c6bfbf6ca1 added invoke.ML;
wenzelm
parents: 19341
diff changeset
    13
use "invoke.ML";