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.
tuned;
authorwenzelm
Tue, 07 Sep 1999 16:56:47 +0200
changeset 7502 257dd7777676
parent 7501 76ed51454609
child 7503 e8be98558eb8
tuned;
src/Pure/Isar/local_defs.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/local_defs.ML	Tue Sep 07 16:56:10 1999 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Sep 07 16:56:47 1999 +0200
@@ -17,7 +17,7 @@
 struct
 
 
-val refl_tac = Tactic.rtac (standard (Drule.reflexive_thm RS Drule.triv_goal));
+val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal));
 
 
 fun gen_def fix prep_term match_binds raw_name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
isabelle