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 signature;
authorwenzelm
Wed, 19 Sep 2018 16:11:54 +0200
changeset 69016 c77efde4e4fd
parent 69015 5eb493b51bf6
child 69017 0c1d7a414185
tuned signature;
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/locale.ML	Tue Sep 18 23:18:20 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 19 16:11:54 2018 +0200
@@ -80,6 +80,7 @@
   val intro_add: attribute
   val unfold_add: attribute
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
+  val try_intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
   type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
@@ -705,7 +706,7 @@
     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
 
 val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
-val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
+val try_intro_locales_tac = gen_intro_locales_tac Method.try_intros_tac;
 
 val _ = Theory.setup
  (Method.setup \<^binding>\<open>intro_locales\<close> (Scan.succeed (METHOD o try_intro_locales_tac false))
isabelle