97 by (rtac refl 1) handle ERROR => writeln"Failed, as expected"; |
97 by (rtac refl 1) handle ERROR => writeln"Failed, as expected"; |
98 getgoal 1; |
98 getgoal 1; |
99 |
99 |
100 |
100 |
101 (*Parallel lifting example. *) |
101 (*Parallel lifting example. *) |
102 goal IFOL.thy "EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)"; |
102 goal IFOL.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"; |
103 by (resolve_tac [exI, allI] 1); |
103 by (resolve_tac [exI, allI] 1); |
104 by (resolve_tac [exI, allI] 1); |
104 by (resolve_tac [exI, allI] 1); |
105 by (resolve_tac [exI, allI] 1); |
105 by (resolve_tac [exI, allI] 1); |
106 by (resolve_tac [exI, allI] 1); |
106 by (resolve_tac [exI, allI] 1); |
107 by (resolve_tac [exI, allI] 1); |
107 by (resolve_tac [exI, allI] 1); |
108 |
108 |
109 |
109 |
110 val prems = |
110 val prems = |
111 goal IFOL.thy "(EX z.F(z)) & B ==> (EX z. F(z) & B)"; |
111 goal IFOL.thy "(EX z. F(z)) & B ==> (EX z. F(z) & B)"; |
112 by (rtac conjE 1); |
112 by (rtac conjE 1); |
113 by (resolve_tac prems 1); |
113 by (resolve_tac prems 1); |
114 by (rtac exE 1); |
114 by (rtac exE 1); |
115 by (assume_tac 1); |
115 by (assume_tac 1); |
116 by (rtac exI 1); |
116 by (rtac exI 1); |