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.
added missing case: meta universal quantifier
authorboehmes
Thu, 08 Apr 2010 22:39:06 +0200
changeset 36099 7e1f972df25f
parent 36098 53992c639da5
child 36100 a8912920ef4f
added missing case: meta universal quantifier
src/HOL/Tools/Qelim/ferrante_rackoff.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Thu Apr 08 08:17:27 2010 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Thu Apr 08 22:39:06 2010 +0200
@@ -187,6 +187,7 @@
    | Const ("op -->", _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
+   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
    | _ => Thm.dest_fun2 tm)
   and find_args bounds tm =
isabelle