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.
tuned comment;
authorwenzelm
Fri, 25 Jul 2014 21:44:03 +0200
changeset 57690 5b652fd305d4
parent 57689 e189ba8a64b9
child 57691 9616643a3032
tuned comment;
src/Pure/Tools/find_theorems.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Tools/find_theorems.ML	Fri Jul 25 21:29:12 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Jul 25 21:44:03 2014 +0200
@@ -182,7 +182,7 @@
       val goal_concl = Logic.concl_of_goal goal 1;
       val rule_mp = hd (Logic.strip_imp_prems rule);
       val rule_concl = Logic.strip_imp_concl rule;
-      fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);  (* FIXME ?? *)
+      fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);  (* FIXME ?!? *)
       val rule_tree = combine rule_mp rule_concl;
       fun goal_tree prem = combine prem goal_concl;
       fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
isabelle