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.
use Rulify.rulify_no_asm;
authorwenzelm
Thu, 07 Sep 2000 20:59:37 +0200
changeset 9904 09253f667beb
parent 9903 d087c8dae285
child 9905 14a71104a498
use Rulify.rulify_no_asm;
TFL/post.sml file | annotate | diff | comparison | revisions 
--- a/TFL/post.sml	Thu Sep 07 20:58:54 2000 +0200
+++ b/TFL/post.sml	Thu Sep 07 20:59:37 2000 +0200
@@ -176,8 +176,8 @@
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
-       val rules' = map (standard o rulify) (R.CONJUNCTS rules)
-   in  {induct = meta_outer (rulify (induction RS spec')),
+       val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules)
+   in  {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')),
         rules = ListPair.zip(rules', rows),
         tcs = (termination_goals rules') @ tcs}
    end
isabelle