src/Provers/splitter.ML
changeset 28839 32d498cf7595
parent 26711 3a478bfa1650
child 29548 02a52ae34b7a
equal deleted inserted replaced
28838:d5db6dfcb34a 28839:32d498cf7595
   103 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
   103 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
   104 
   104 
   105 val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
   105 val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
   106   [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
   106   [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
   107   (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
   107   (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
   108   (fn {prems = [prem], ...} => rewtac prem THEN rtac reflexive_thm 1)
   108   (fn {prems, ...} => rewrite_goals_tac prems THEN rtac reflexive_thm 1)
   109 
   109 
   110 val trlift = lift RS transitive_thm;
   110 val trlift = lift RS transitive_thm;
   111 val _ $ (P $ _) $ _ = concl_of trlift;
   111 val _ $ (P $ _) $ _ = concl_of trlift;
   112 
   112 
   113 
   113