src/CTT/Bool.ML
changeset 17441 5b5feca0344a
parent 9251 bd57acd44fc1
     1.1 --- a/src/CTT/Bool.ML	Fri Sep 16 21:02:15 2005 +0200
     1.2 +++ b/src/CTT/Bool.ML	Fri Sep 16 23:01:29 2005 +0200
     1.3 @@ -2,8 +2,6 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1991  University of Cambridge
     1.7 -
     1.8 -The two-element type (booleans and conditionals)
     1.9  *)
    1.10  
    1.11  val bool_defs = [Bool_def,true_def,false_def,cond_def];
    1.12 @@ -27,7 +25,7 @@
    1.13  qed "boolI_false";
    1.14  
    1.15  (*elimination rule: typing of cond*)
    1.16 -Goalw bool_defs 
    1.17 +Goalw bool_defs
    1.18      "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)";
    1.19  by (typechk_tac []);
    1.20  by (ALLGOALS (etac TE));
    1.21 @@ -43,7 +41,7 @@
    1.22  
    1.23  (*computation rules for true, false*)
    1.24  
    1.25 -Goalw bool_defs 
    1.26 +Goalw bool_defs
    1.27      "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)";
    1.28  by (resolve_tac comp_rls 1);
    1.29  by (typechk_tac []);
    1.30 @@ -58,6 +56,3 @@
    1.31  by (ALLGOALS (etac TE));
    1.32  by (typechk_tac []) ;
    1.33  qed "boolC_false";
    1.34 -
    1.35 -writeln"Reached end of file.";
    1.36 -