src/Pure/pure_thy.ML
changeset 15975 cc4821a9f1b1
parent 15964 f2074e12d1d4
child 16023 66561f6814bd
equal deleted inserted replaced
15974:cef3d89d49d4 15975:cc4821a9f1b1
     1 (*  Title:      Pure/pure_thy.ML
     1 (*  Title:      Pure/pure_thy.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4                 contributions by Rafal Kolanski, NICTA
       
     5 
     4 
     6 Theorem database, derived theory operations, and the ProtoPure theory.
     5 Theorem database, derived theory operations, and the ProtoPure theory.
     7 *)
     6 *)
     8 
     7 
     9 signature BASIC_PURE_THY =
     8 signature BASIC_PURE_THY =