Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Cube/ex/ex.ML
changeset 11260 b736de4cb913
parent 4583 6d9be46ea566
child 15531 08c8dad8e399
equal deleted inserted replaced
11259:27f0f16f8003 11260:b736de4cb913 
   118 
   118 
   119 goal L2.thy "A:* B:* |- Pi C:*.(A->B->C)->C : ?T";
 
   119 goal L2.thy "A:* B:* |- Pi C:*.(A->B->C)->C : ?T";
 
   120 by (DEPTH_SOLVE (ares_tac L2 1));
 
   120 by (DEPTH_SOLVE (ares_tac L2 1));
 
   121 uresult();
 
   121 uresult();
 
   122 
   122 
   123 goal LOmega.thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T";
 
   123 goal Lomega2.thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T";
 
   124 by (DEPTH_SOLVE (ares_tac LOmega 1));
 
   124 by (DEPTH_SOLVE (ares_tac Lomega2 1));
 
   125 uresult();
 
   125 uresult();
 
   126 
   126 
   127 goal LOmega.thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
 
   127 goal Lomega2.thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
 
   128 by (DEPTH_SOLVE (ares_tac LOmega 1));
 
   128 by (DEPTH_SOLVE (ares_tac Lomega2 1));
 
   129 uresult();
 
   129 uresult();
 
   130 
   130 
   131 goal LOmega.thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))";
 
   131 goal Lomega2.thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))";
 
   132 by (strip_asms_tac LOmega 1);
 
   132 by (strip_asms_tac Lomega2 1);
 
   133 by (rtac lam_ss 1);
 
   133 by (rtac lam_ss 1);
 
   134 by (DEPTH_SOLVE_1(ares_tac LOmega 1));
 
   134 by (DEPTH_SOLVE_1(ares_tac Lomega2 1));
 
   135 by (DEPTH_SOLVE_1(ares_tac LOmega 2));
 
   135 by (DEPTH_SOLVE_1(ares_tac Lomega2 2));
 
   136 by (rtac lam_ss 1);
 
   136 by (rtac lam_ss 1);
 
   137 by (DEPTH_SOLVE_1(ares_tac LOmega 1));
 
   137 by (DEPTH_SOLVE_1(ares_tac Lomega2 1));
 
   138 by (DEPTH_SOLVE_1(ares_tac LOmega 2));
 
   138 by (DEPTH_SOLVE_1(ares_tac Lomega2 2));
 
   139 by (rtac lam_ss 1);
 
   139 by (rtac lam_ss 1);
 
   140 by (assume_tac 1);
 
   140 by (assume_tac 1);
 
   141 by (DEPTH_SOLVE_1(ares_tac LOmega 2));
 
   141 by (DEPTH_SOLVE_1(ares_tac Lomega2 2));
 
   142 by (etac pi_elim 1);
 
   142 by (etac pi_elim 1);
 
   143 by (assume_tac 1);
 
   143 by (assume_tac 1);
 
   144 by (etac pi_elim 1);
 
   144 by (etac pi_elim 1);
 
   145 by (assume_tac 1);
 
   145 by (assume_tac 1);
 
   146 by (assume_tac 1);
 
   146 by (assume_tac 1);
isabelle