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.
has_meta_prems: include "==";
authorwenzelm
Fri, 10 Nov 2000 19:10:34 +0100
changeset 10442 8ef083987af9
parent 10441 d727c39c4a4b
child 10443 0a68dc9edba5
has_meta_prems: include "==";
src/Pure/logic.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/logic.ML	Fri Nov 10 19:09:40 2000 +0100
+++ b/src/Pure/logic.ML	Fri Nov 10 19:10:34 2000 +0100
@@ -256,6 +256,7 @@
 fun has_meta_prems prop i =
   let
     fun is_meta (Const ("==>", _) $ _ $ _) = true
+      | is_meta (Const ("==", _) $ _ $ _) = true
       | is_meta (Const ("all", _) $ _) = true
       | is_meta _ = false;
     val horn = skip_flexpairs prop;
isabelle