src/HOL/UNITY/Lift.ML
changeset 6024 cb87f103d114
parent 5783 95ac0bf10518
child 6061 e80bcb98df78
     1.1 --- a/src/HOL/UNITY/Lift.ML	Fri Dec 11 10:38:51 1998 +0100
     1.2 +++ b/src/HOL/UNITY/Lift.ML	Fri Dec 11 10:41:53 1998 +0100
     1.3 @@ -435,4 +435,4 @@
     1.4  by (Blast_tac 1);
     1.5  qed "lift_1";
     1.6  
     1.7 -Close_locale();
     1.8 +Close_locale "floor";