equal
deleted
inserted
replaced
150 Simplifier.simproc @{theory} "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 Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule |
156 |> map (standard #> RuleCases.save rule); |
156 |> map (standard #> RuleCases.save rule); |
157 |
157 |
158 val supp_prod = thm "supp_prod"; |
158 val supp_prod = thm "supp_prod"; |
159 val fresh_prod = thm "fresh_prod"; |
159 val fresh_prod = thm "fresh_prod"; |
160 val supports_fresh = thm "supports_fresh"; |
160 val supports_fresh = thm "supports_fresh"; |