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.
new Close_locale synatx
authorpaulson
Fri, 11 Dec 1998 10:34:03 +0100
changeset 6021 4a3fc834288e
parent 6020 4b109bf75976
child 6022 259e4f2114e1
new Close_locale synatx
src/ZF/AC/AC16_WO4.ML file | annotate | diff | comparison | revisions
src/ZF/AC/DC.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/AC/AC16_WO4.ML	Mon Dec 07 18:26:46 1998 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Fri Dec 11 10:34:03 1998 +0100
@@ -603,7 +603,7 @@
 		      all_in_lepoll_m, OUN_eq_x] 1));
 qed "conclusion";
 
-Close_locale ();
+Close_locale "AC16";
 
 
 
--- a/src/ZF/AC/DC.ML	Mon Dec 07 18:26:46 1998 +0100
+++ b/src/ZF/AC/DC.ML	Fri Dec 11 10:34:03 1998 +0100
@@ -144,7 +144,7 @@
                             (2, image_fun RS sym)]) 1);
 qed "lemma3";
 
-Close_locale();
+Close_locale "DC0_imp";
 
 Goalw [DC_def, DC0_def] "DC0 ==> DC(nat)";
 by (Clarify_tac 1);
@@ -411,7 +411,7 @@
         addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1);
 qed "lemma3";
 
-Close_locale();
+Close_locale "imp_DC0";
 
 
 Goalw [DC_def, DC0_def] "DC(nat) ==> DC0";
isabelle