src/HOLCF/One.ML
changeset 12030 46d57d0290a2
parent 9248 e1dee89de037
child 14981 e73f8140af78
     1.1 --- a/src/HOLCF/One.ML	Sat Nov 03 01:40:28 2001 +0100
     1.2 +++ b/src/HOLCF/One.ML	Sat Nov 03 01:41:26 2001 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4  (*  Title:      HOLCF/One.ML
     1.5      ID:         $Id$
     1.6      Author:     Oscar Slotosch
     1.7 -    Copyright   1997 Technische Universitaet Muenchen
     1.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  
    1.10 -The unit domain
    1.11 +The unit domain.
    1.12  *)
    1.13  
    1.14  (* ------------------------------------------------------------------------ *)
    1.15 @@ -11,7 +11,7 @@
    1.16  (* ------------------------------------------------------------------------ *)
    1.17  
    1.18  Goalw [ONE_def] "t=UU | t = ONE";
    1.19 -by (lift.induct_tac "t" 1);
    1.20 +by (induct_tac "t" 1);
    1.21  by (Simp_tac 1);
    1.22  by (Simp_tac 1);
    1.23  qed "Exh_one";