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.
fixed qed;
authorwenzelm
Tue, 28 Oct 1997 17:41:40 +0100
changeset 4025 77e426be5624
parent 4024 3c056eab237c
child 4026 b94dc94be4b7
fixed qed;
src/HOL/HOL.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.ML	Tue Oct 28 17:41:15 1997 +0100
+++ b/src/HOL/HOL.ML	Tue Oct 28 17:41:40 1997 +0100
@@ -77,7 +77,7 @@
 qed_goalw "TrueI" HOL.thy [True_def] "True"
   (fn _ => [rtac refl 1]);
 
-qed_goal "eqTrueI " HOL.thy "P ==> P=True" 
+qed_goal "eqTrueI" HOL.thy "P ==> P=True" 
  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
 
 qed_goal "eqTrueE" HOL.thy "P=True ==> P"
isabelle