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, 28 Mar 2023 19:07:58 +0200
changeset 77733 59c94a376a3c
parent 77732 7d014af40072
child 77734 c4c96a833a37
tuned;
src/Pure/General/set.ML file | annotate | diff | comparison | revisions
src/Pure/General/table.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/General/set.ML	Tue Mar 28 19:03:39 2023 +0200
+++ b/src/Pure/General/set.ML	Tue Mar 28 19:07:58 2023 +0200
@@ -33,6 +33,8 @@
 functor Set(Key: KEY): SET =
 struct
 
+(* keys *)
+
 structure Key = Key;
 type elem = Key.key;
 
--- a/src/Pure/General/table.ML	Tue Mar 28 19:03:39 2023 +0200
+++ b/src/Pure/General/table.ML	Tue Mar 28 19:07:58 2023 +0200
@@ -67,9 +67,13 @@
 functor Table(Key: KEY): TABLE =
 struct
 
+(* keys *)
+
 structure Key = Key;
 type key = Key.key;
 
+exception DUP of key;
+
 
 (* datatype *)
 
@@ -78,8 +82,6 @@
   Branch2 of 'a table * (key * 'a) * 'a table |
   Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
 
-exception DUP of key;
-
 
 (* empty and single *)
isabelle