equal
deleted
inserted
replaced
96 |
96 |
97 *************************************************************) |
97 *************************************************************) |
98 |
98 |
99 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *) |
99 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *) |
100 |
100 |
101 val lift = Goal.prove_global \<^theory>\<open>Pure\<close> ["P", "Q", "R"] |
101 val lift = Goal.prove_global \<^theory> ["P", "Q", "R"] |
102 [Syntax.read_prop_global \<^theory>\<open>Pure\<close> "!!x :: 'b. Q(x) == R(x) :: 'c"] |
102 [Syntax.read_prop_global \<^theory>\<open>Pure\<close> "!!x :: 'b. Q(x) == R(x) :: 'c"] |
103 (Syntax.read_prop_global \<^theory>\<open>Pure\<close> "P(%x. Q(x)) == P(%x. R(x))") |
103 (Syntax.read_prop_global \<^theory>\<open>Pure\<close> "P(%x. Q(x)) == P(%x. R(x))") |
104 (fn {context = ctxt, prems} => |
104 (fn {context = ctxt, prems} => |
105 rewrite_goals_tac ctxt prems THEN resolve_tac ctxt [reflexive_thm] 1) |
105 rewrite_goals_tac ctxt prems THEN resolve_tac ctxt [reflexive_thm] 1) |
106 |
106 |