changeset 48891 | c0eafbd55de3 |
parent 41526 | 54b4686704af |
child 51308 | 51e158e988a5 |
--- a/src/CTT/CTT.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/CTT/CTT.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,9 +7,9 @@ theory CTT imports Pure -uses "~~/src/Provers/typedsimp.ML" ("rew.ML") begin +ML_file "~~/src/Provers/typedsimp.ML" setup Pure_Thy.old_appl_syntax_setup typedecl i @@ -460,7 +460,7 @@ fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms) *} -use "rew.ML" +ML_file "rew.ML" subsection {* The elimination rules for fst/snd *}