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.
avoid reference to internal skolem;
authorwenzelm
Tue, 11 Jul 2006 23:49:32 +0200
changeset 20103 26747ea32d35
parent 20102 6676a17dfc88
child 20104 f8e7c71926e4
avoid reference to internal skolem;
src/HOL/Bali/AxCompl.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Bali/AxCompl.thy	Tue Jul 11 23:00:39 2006 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Tue Jul 11 23:49:32 2006 +0200
@@ -1159,7 +1159,7 @@
 	apply (rule ax_derivs.BinOp)
 	apply  (erule MGFnD [THEN ax_NormalD])
 	apply (rule allI)
-	apply (case_tac "need_second_arg binop__ v1")
+	apply (case_tac "need_second_arg binop v1")
 	apply  simp
 	apply  (erule MGFnD' [THEN conseq12])
 	apply  (fastsimp intro: eval.BinOp)
isabelle