Mercurial Mercurial > hg > nominal2 / 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.
More higher order unification problems
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Sat, 17 Oct 2009 12:44:58 +0200
changeset 123 50219e796e05
parent 122 768c5d319a0a
child 124 de944fcd6a05
More higher order unification problems
QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/QuotMain.thy	Sat Oct 17 12:31:48 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 12:44:58 2009 +0200
@@ -1237,7 +1237,11 @@
 prefer 3
 (* APPLY_RSP *)
 thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]
-apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+(* MINE *)
+prefer 4
+apply (rule list_eq_refl )
+
 sorry
 
 thm list.recs(2)
nominal2