moved datatype realizer to 'old_datatype' and colleagues
authorblanchet
Thu Sep 18 16:47:40 2014 +0200 (2014-09-18)
changeset 58376c9d3074f83b3
parent 58375 7b92932ffea5
child 58377 c6f93b8d2d8e
moved datatype realizer to 'old_datatype' and colleagues
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Library/Old_Datatype.thy
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 18 16:47:40 2014 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 18 16:47:40 2014 +0200
     1.3 @@ -232,7 +232,6 @@
     1.4  ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
     1.5  ML_file "Tools/BNF/bnf_lfp_size.ML"
     1.6  ML_file "Tools/Function/old_size.ML"
     1.7 -ML_file "Tools/datatype_realizer.ML"
     1.8  
     1.9  hide_fact (open) id_transfer
    1.10  
     2.1 --- a/src/HOL/Library/Old_Datatype.thy	Thu Sep 18 16:47:40 2014 +0200
     2.2 +++ b/src/HOL/Library/Old_Datatype.thy	Thu Sep 18 16:47:40 2014 +0200
     2.3 @@ -523,5 +523,6 @@
     2.4  
     2.5  ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
     2.6  ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
     2.7 +ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
     2.8  
     2.9  end