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
Sun, 01 Nov 2009 16:23:31 +0100
changeset 33370 69531a7b55b6
parent 33369 470a7b233ee5
child 33371 d74dc1b54930
tuned signature;
src/Pure/Isar/context_rules.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/context_rules.ML	Sun Nov 01 15:44:26 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML	Sun Nov 01 16:23:31 2009 +0100
@@ -7,8 +7,7 @@
 
 signature CONTEXT_RULES =
 sig
-  type netpair
-  type T
+  type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net
   val netpair_bang: Proof.context -> netpair
   val netpair: Proof.context -> netpair
   val orderlist: ((int * int) * 'a) list -> 'a list
@@ -65,7 +64,7 @@
 type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
 val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
 
-datatype T = Rules of
+datatype rules = Rules of
  {next: int,
   rules: (int * ((int * bool) * thm)) list,
   netpairs: netpair list,
@@ -92,7 +91,7 @@
 
 structure Rules = GenericDataFun
 (
-  type T = T;
+  type T = rules;
   val empty = make_rules ~1 [] empty_netpairs ([], []);
   val extend = I;
isabelle