added Tools/named_thms.ML;
authorwenzelm
Sun, 29 Jul 2007 14:30:02 +0200
changeset 24046 10f681043e07
parent 24045 bead02a55952
child 24047 47b588ce11ec
added Tools/named_thms.ML;
src/Pure/IsaMakefile
src/Pure/Tools/ROOT.ML
--- a/src/Pure/IsaMakefile	Sun Jul 29 14:30:01 2007 +0200
+++ b/src/Pure/IsaMakefile	Sun Jul 29 14:30:02 2007 +0200
@@ -61,9 +61,9 @@
   Tools/class_package.ML Tools/codegen_consts.ML Tools/codegen_data.ML		\
   Tools/codegen_func.ML Tools/codegen_funcgr.ML Tools/codegen_names.ML		\
   Tools/codegen_package.ML Tools/codegen_serializer.ML Tools/codegen_thingol.ML	\
-  Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML		\
-  Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML		\
-  compress.ML config_option.ML conjunction.ML consts.ML context.ML		\
+  Tools/invoke.ML Tools/named_thms.ML Tools/nbe.ML Tools/nbe_codegen.ML		\
+  Tools/nbe_eval.ML Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML 	\
+  codegen.ML compress.ML config_option.ML conjunction.ML consts.ML context.ML	\
   context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML		\
   fact_index.ML goal.ML install_pp.ML library.ML logic.ML meta_simplifier.ML	\
   more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML	\
--- a/src/Pure/Tools/ROOT.ML	Sun Jul 29 14:30:01 2007 +0200
+++ b/src/Pure/Tools/ROOT.ML	Sun Jul 29 14:30:02 2007 +0200
@@ -4,6 +4,8 @@
 Miscellaneous tools and packages for Pure Isabelle.
 *)
 
+use "named_thms.ML";
+
 (*basic XML support*)
 use "xml.ML";
 use "xml_syntax.ML";