Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Mon, 01 Oct 2018 16:40:45 +0200
changeset 69100 0b0c3dfd730f
parent 69099 d44cb8a3e5e0
child 69101 991a3feaf270
tuned;
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/drule.ML	Mon Oct 01 12:41:35 2018 +0200
+++ b/src/Pure/drule.ML	Mon Oct 01 16:40:45 2018 +0200
@@ -141,7 +141,7 @@
 
 (*cterm version of list_implies: [A1,...,An], B  goes to \<lbrakk>A1;...;An\<rbrakk>\<Longrightarrow>B *)
 fun list_implies([], B) = B
-  | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
+  | list_implies(A::As, B) = mk_implies (A, list_implies(As,B));
 
 (*cterm version of list_comb: maps  (f, [t1,...,tn])  to  f(t1,...,tn) *)
 fun list_comb (f, []) = f
isabelle