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 comments;
authorwenzelm
Wed, 04 Apr 2012 17:14:19 +0200
changeset 47337 bd24e466bef9
parent 47336 bed4b2738d8a
child 47338 e331c6256a41
tuned comments;
src/Pure/global_theory.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/global_theory.ML	Wed Apr 04 14:19:47 2012 +0200
+++ b/src/Pure/global_theory.ML	Wed Apr 04 17:14:19 2012 +0200
@@ -49,7 +49,7 @@
 
 (** theory data **)
 
-type proofs = thm list * unit lazy;
+type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
 
 val empty_proofs: proofs = ([], Lazy.value ());
 
@@ -61,7 +61,7 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T * (proofs * proofs);
+  type T = Facts.T * (proofs * proofs);  (*facts, recent proofs, all proofs of theory node*)
   val empty = (Facts.empty, (empty_proofs, empty_proofs));
   fun extend (facts, _) = (facts, snd empty);
   fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), snd empty);
isabelle