src/Pure/Isar/subgoal.ML
changeset 67721 5348bea4accd
parent 67649 1e1782c1aedf
child 71945 8ed68b2aeba1
equal deleted inserted replaced
67719:17874d43d3b3 67721:5348bea4accd
   106   in ((inst2, th''), ctxt'') end;
   106   in ((inst2, th''), ctxt'') end;
   107 
   107 
   108 (*
   108 (*
   109        [x, A x]
   109        [x, A x]
   110           :
   110           :
   111        B x ==> C
   111        B x \<Longrightarrow> C
   112   ------------------
   112   ------------------
   113   [!!x. A x ==> B x]
   113   [\<And>x. A x \<Longrightarrow> B x]
   114           :
   114           :
   115           C
   115           C
   116 *)
   116 *)
   117 fun lift_subgoals ctxt params asms th =
   117 fun lift_subgoals ctxt params asms th =
   118   let
   118   let