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.
for now safely but unpractically assume no predicate is terminating
authorbulwahn
Thu, 21 Oct 2010 19:13:08 +0200
changeset 40050 638ce4dabe53
parent 40049 75d9f57123d6
child 40051 b6acda4d1c29
for now safely but unpractically assume no predicate is terminating
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:07 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:08 2010 +0200
@@ -1982,7 +1982,7 @@
 
 fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
   let
-    val is_terminating = true (* FIXME: requires an termination analysis *)  
+    val is_terminating = false (* FIXME: requires an termination analysis *)  
     val compilation_modifiers =
       (if pol then compilation_modifiers else
         negative_comp_modifiers_of compilation_modifiers)
isabelle