Mercurial Mercurial > hg > nominal2 / 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.
further simplification
authorChristian Urban <urbanc@in.tum.de>
Thu, 03 Dec 2009 02:53:54 +0100
changeset 491 3a4da8a63840
parent 490 5214ec75add4
child 492 6793659d38d6
further simplification
QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/QuotMain.thy	Thu Dec 03 02:18:21 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 02:53:54 2009 +0100
@@ -1121,10 +1121,7 @@
 *}
 
 ML {*
-fun lambda_prs_tac quot ctxt = CONVERSION
-    (Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (lambda_prs_conv quot ctxt) then_conv
-          Conv.concl_conv ~1 (lambda_prs_conv quot ctxt))) ctxt) 
+fun lambda_prs_tac quot ctxt = CONVERSION (lambda_prs_conv quot ctxt)
 *}
 
 (*
nominal2