# HG changeset patch # User paulson # Date 913368843 -3600 # Node ID 4a3fc834288ea23d3cdfd0166d111e7a2e523b48 # Parent 4b109bf7597664d951e7689a28f5b8c171cee81e new Close_locale synatx diff -r 4b109bf75976 -r 4a3fc834288e src/ZF/AC/AC16_WO4.ML --- 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"; diff -r 4b109bf75976 -r 4a3fc834288e src/ZF/AC/DC.ML --- 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";