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.
now uses the identity function
authorpaulson
Wed, 08 Sep 1999 15:44:11 +0200
changeset 7520 65f0cec65fc6
parent 7519 8e4a21d1ba4f
child 7521 a18adacbdbd2
now uses the identity function
src/HOL/UNITY/Common.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/UNITY/Common.ML	Wed Sep 08 15:41:58 1999 +0200
+++ b/src/HOL/UNITY/Common.ML	Wed Sep 08 15:44:11 1999 +0200
@@ -73,7 +73,7 @@
 \               n: common |]  \
 \     ==> F : (atMost n) LeadsTo common";
 by (rtac LeadsTo_weaken_R 1);
-by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
+by (res_inst_tac [("f","id"), ("l","n")] GreaterThan_bounded_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (rtac subset_refl 2);
 by (blast_tac (claset() addDs [PSP_Stable2]
isabelle