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.
proper syntax declaration
authorhaftmann
Fri, 21 Aug 2020 18:59:29 +0000
changeset 72186 bdf77466b6c8
parent 72185 0f9ebade33ab
child 72187 e4aecb0c7296
proper syntax declaration
src/HOL/Statespace/state_space.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Statespace/state_space.ML	Fri Aug 21 12:43:07 2020 +0100
+++ b/src/HOL/Statespace/state_space.ML	Fri Aug 21 18:59:29 2020 +0000
@@ -299,7 +299,7 @@
 fun add_declaration name decl thy =
   thy
   |> Named_Target.init name
-  |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
+  |> (fn lthy => Local_Theory.declaration {syntax = true, pervasive = false} (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
 fun parent_components thy (Ts, pname, renaming) =
isabelle