equal
deleted
inserted
replaced
230 ML_file "Tools/BNF/bnf_lfp.ML" |
230 ML_file "Tools/BNF/bnf_lfp.ML" |
231 ML_file "Tools/BNF/bnf_lfp_compat.ML" |
231 ML_file "Tools/BNF/bnf_lfp_compat.ML" |
232 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" |
232 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" |
233 ML_file "Tools/BNF/bnf_lfp_size.ML" |
233 ML_file "Tools/BNF/bnf_lfp_size.ML" |
234 ML_file "Tools/Function/old_size.ML" |
234 ML_file "Tools/Function/old_size.ML" |
235 ML_file "Tools/datatype_realizer.ML" |
|
236 |
235 |
237 hide_fact (open) id_transfer |
236 hide_fact (open) id_transfer |
238 |
237 |
239 end |
238 end |