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.
Updated comments.
authorballarin
Thu, 03 Aug 2006 14:53:57 +0200
changeset 20317 6e070b33e72b
parent 20316 99b6e2900c0f
child 20318 0e0ea63fe768
Updated comments.
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/locale.ML	Thu Aug 03 14:53:35 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 03 14:53:57 2006 +0200
@@ -32,8 +32,6 @@
 - beta-eta normalisation of interpretation parameters
 - dangling type frees in locales
 - test subsumption of interpretations when merging theories
-- var vs. fixes in locale to be interpreted (interpretation in locale)
-  (implicit locale expressions generated by multiple registrations)
 *)
 
 signature LOCALE =
@@ -160,7 +158,8 @@
 type locale =
  {axiom: Element.witness list,
     (* For locales that define predicates this is [A [A]], where A is the locale
-       specification.  Otherwise []. *)
+       specification.  Otherwise [].
+       Only required to generate the right witnesses for locales with predicates. *)
   import: expr,                                                     (*dynamic import*)
   elems: (Element.context_i * stamp) list,
     (* Static content, neither Fixes nor Constrains elements *)
isabelle