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.
ZF/indrule/mk_pred_typ: corrected pattern to include Abs, allowing it to
authorlcp
Fri, 06 May 1994 15:49:23 +0200
changeset 366 5b6e4340085b
parent 365 796c5e305b31
child 367 b734dc03067e
ZF/indrule/mk_pred_typ: corrected pattern to include Abs, allowing it to handle any number of right-nested Sigmas.
src/ZF/indrule.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/indrule.ML	Fri May 06 15:35:35 1994 +0200
+++ b/src/ZF/indrule.ML	Fri May 06 15:49:23 1994 +0200
@@ -77,7 +77,7 @@
 (*Make distinct predicates for each inductive set*)
 
 (*Sigmas and Cartesian products may nest ONLY to the right!*)
-fun mk_pred_typ (t $ A $ B) = 
+fun mk_pred_typ (t $ A $ Abs(_,_,B)) = 
         if t = Pr.sigma  then  iT --> mk_pred_typ B
                          else  iT --> oT
   | mk_pred_typ _           =  iT --> oT
isabelle