# HG changeset patch
# User blanchet
# Date 1514906233 -3600
# Node ID 07176d5b81d51df16e7aba0952c01307f6f74302
# Parent  0ee38196509ece137664184c9ae1b1d1ed0ce3e2
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction

diff -r 0ee38196509e -r 07176d5b81d5 src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Tue Jan 02 16:11:20 2018 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Tue Jan 02 16:17:13 2018 +0100
@@ -9,9 +9,6 @@
 imports Main
 begin
 
-ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
-ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
-
 
 subsection \<open>The datatype universe\<close>
 
diff -r 0ee38196509e -r 07176d5b81d5 src/HOL/Library/Realizers.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Realizers.thy	Tue Jan 02 16:17:13 2018 +0100
@@ -0,0 +1,14 @@
+(*  Title:      HOL/Library/Realizers.thy
+    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
+*)
+
+section \<open>Program extraction from proofs involving datatypes and inductive predicates\<close>
+
+theory Realizers
+imports Main
+begin
+
+ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
+ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
+
+end
diff -r 0ee38196509e -r 07176d5b81d5 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jan 02 16:11:20 2018 +0100
+++ b/src/HOL/ROOT	Tue Jan 02 16:17:13 2018 +0100
@@ -19,7 +19,7 @@
   sessions
     "HOL-Library"
   theories
-    "HOL-Library.Old_Datatype"
+    "HOL-Library.Realizers"
 
 session "HOL-Library" (main timing) in Library = HOL +
   description {*
@@ -52,6 +52,7 @@
     (*legacy tools*)
     Old_Datatype
     Old_Recdef
+    Realizers
     Refute
   document_files "root.bib" "root.tex"