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.
Removed unnecessary application of Drule.standard.
authorberghofe
Wed, 10 Oct 2001 18:40:46 +0200
changeset 11718 92706a69dacc
parent 11717 d808005e6e08
child 11719 49c14348a42b
Removed unnecessary application of Drule.standard.
src/Pure/Isar/local_defs.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/local_defs.ML	Wed Oct 10 18:39:38 2001 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Oct 10 18:40:46 2001 +0200
@@ -22,7 +22,7 @@
 
 local
 
-val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal));
+val refl_tac = Tactic.rtac (Drule.reflexive_thm RS Drule.triv_goal);
 
 fun dest_lhs cprop =
   let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop)))
isabelle