src/FOLP/ex/If.ML
changeset 17480 fd19f77dcf60
parent 5061 f947332d5465
     1.1 --- a/src/FOLP/ex/If.ML	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ b/src/FOLP/ex/If.ML	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -1,20 +1,15 @@
     1.4 -(*  Title:      FOLP/ex/if
     1.5 +(*  Title:      FOLP/ex/If.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1991  University of Cambridge
     1.9 -
    1.10 -For ex/if.thy.  First-Order Logic: the 'if' example
    1.11  *)
    1.12  
    1.13 -open If;
    1.14 -open Cla;    (*in case structure Int is open!*)
    1.15 -
    1.16 -val prems = goalw If.thy [if_def]
    1.17 +val prems = goalw (the_context ()) [if_def]
    1.18      "[| !!x. x:P ==> f(x):Q; !!x. x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
    1.19  by (fast_tac (FOLP_cs addIs prems) 1);
    1.20  val ifI = result();
    1.21  
    1.22 -val major::prems = goalw If.thy [if_def]
    1.23 +val major::prems = goalw (the_context ()) [if_def]
    1.24     "[| p:if(P,Q,R);  !!x y.[| x:P; y:Q |] ==> f(x,y):S; \
    1.25  \                    !!x y.[| x:~P; y:R |] ==> g(x,y):S |] ==> ?p:S";
    1.26  by (cut_facts_tac [major] 1);
    1.27 @@ -39,5 +34,3 @@
    1.28  Goal "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
    1.29  by (fast_tac if_cs 1);
    1.30  val nested_ifs = result();
    1.31 -
    1.32 -writeln"Reached end of file.";