equal
deleted
inserted
replaced
145 else NONE |
145 else NONE |
146 end |
146 end |
147 | perm_simproc' thy ss _ = NONE; |
147 | perm_simproc' thy ss _ = NONE; |
148 |
148 |
149 val perm_simproc = |
149 val perm_simproc = |
150 Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc'; |
150 Simplifier.simproc @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc'; |
151 |
151 |
152 val meta_spec = thm "meta_spec"; |
152 val meta_spec = thm "meta_spec"; |
153 |
153 |
154 fun projections rule = |
154 fun projections rule = |
155 ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule |
155 ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule |