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