# HG changeset patch
# User wenzelm
# Date 898187325 -7200
# Node ID e925308df78be48e843a5fe57af7499b441dc5ca
# Parent  bde086cfa597810c8ffa9fcf50ea8ed0cc4945c5
isatool fixgoal;

diff -r bde086cfa597 -r e925308df78b src/FOL/ex/If.ML
--- a/src/FOL/ex/If.ML	Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/If.ML	Thu Jun 18 18:28:45 1998 +0200
@@ -21,7 +21,7 @@
 qed "ifE";
 
 
-goal If.thy
+Goal
     "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
 by (rtac iffI 1);
 by (etac ifE 1);
@@ -36,7 +36,7 @@
 qed "if_commute";
 
 
-goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
+Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
 by (Blast_tac 1);
 qed "nested_ifs";
 
@@ -47,7 +47,7 @@
 
 
 (*An invalid formula.  High-level rules permit a simpler diagnosis*)
-goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
+Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
 by (Blast_tac 1) handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
 getgoal 1; 
diff -r bde086cfa597 -r e925308df78b src/FOL/ex/List.ML
--- a/src/FOL/ex/List.ML	Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/List.ML	Thu Jun 18 18:28:45 1998 +0200
@@ -17,49 +17,49 @@
 	  hd_eq, tl_eq, forall_nil, forall_cons, list_free,
 	  len_nil, len_cons, at_0, at_succ];
 
-goal List.thy "~l=[] --> hd(l).tl(l) = l";
+Goal "~l=[] --> hd(l).tl(l) = l";
 by (IND_TAC list_exh Simp_tac "l" 1);
 result();
 
-goal List.thy "(l1++l2)++l3 = l1++(l2++l3)";
+Goal "(l1++l2)++l3 = l1++(l2++l3)";
 by (IND_TAC list_ind Simp_tac "l1" 1);
 qed "append_assoc";
 
-goal List.thy "l++[] = l";
+Goal "l++[] = l";
 by (IND_TAC list_ind Simp_tac "l" 1);
 qed "app_nil_right";
 
-goal List.thy "l1++l2=[] <-> l1=[] & l2=[]";
+Goal "l1++l2=[] <-> l1=[] & l2=[]";
 by (IND_TAC list_exh Simp_tac "l1" 1);
 qed "app_eq_nil_iff";
 
-goal List.thy "forall(l++l',P) <-> forall(l,P) & forall(l',P)";
+Goal "forall(l++l',P) <-> forall(l,P) & forall(l',P)";
 by (IND_TAC list_ind Simp_tac "l" 1);
 qed "forall_app";
 
-goal List.thy "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
+Goal "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
 by (IND_TAC list_ind Simp_tac "l" 1);
 by (Fast_tac 1);
 qed "forall_conj";
 
-goal List.thy "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)";
+Goal "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)";
 by (IND_TAC list_ind Simp_tac "l" 1);
 qed "forall_ne";
 
 (*** Lists with natural numbers ***)
 
-goal List.thy "len(l1++l2) = len(l1)+len(l2)";
+Goal "len(l1++l2) = len(l1)+len(l2)";
 by (IND_TAC list_ind Simp_tac "l1" 1);
 qed "len_app";
 
-goal List.thy "i<len(l1) --> at(l1++l2,i) = at(l1,i)";
+Goal "i<len(l1) --> at(l1++l2,i) = at(l1,i)";
 by (IND_TAC list_ind Simp_tac "l1" 1);
 by (REPEAT (rtac allI 1));
 by (rtac impI 1);
 by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
 qed "at_app1";
 
-goal List.thy "at(l1++(x . l2), len(l1)) = x";
+Goal "at(l1++(x . l2), len(l1)) = x";
 by (IND_TAC list_ind Simp_tac "l1" 1);
 qed "at_app_hd2";
 
diff -r bde086cfa597 -r e925308df78b src/FOL/ex/Nat.ML
--- a/src/FOL/ex/Nat.ML	Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/Nat.ML	Thu Jun 18 18:28:45 1998 +0200
@@ -11,7 +11,7 @@
 
 open Nat;
 
-goal Nat.thy "Suc(k) ~= k";
+Goal "Suc(k) ~= k";
 by (res_inst_tac [("n","k")] induct 1);
 by (rtac notI 1);
 by (etac Suc_neq_0 1);
@@ -21,7 +21,7 @@
 qed "Suc_n_not_n";
 
 
-goal Nat.thy "(k+m)+n = k+(m+n)";
+Goal "(k+m)+n = k+(m+n)";
 prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
 by (rtac induct 1);
 back();
@@ -31,29 +31,29 @@
 back();
 back();
 
-goalw Nat.thy [add_def] "0+n = n";
+Goalw [add_def] "0+n = n";
 by (rtac rec_0 1);
 qed "add_0";
 
-goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
+Goalw [add_def] "Suc(m)+n = Suc(m+n)";
 by (rtac rec_Suc 1);
 qed "add_Suc";
 
 Addsimps [add_0, add_Suc];
 
-goal Nat.thy "(k+m)+n = k+(m+n)";
+Goal "(k+m)+n = k+(m+n)";
 by (res_inst_tac [("n","k")] induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "add_assoc";
 
-goal Nat.thy "m+0 = m";
+Goal "m+0 = m";
 by (res_inst_tac [("n","m")] induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "add_0_right";
 
-goal Nat.thy "m+Suc(n) = Suc(m+n)";
+Goal "m+Suc(n) = Suc(m+n)";
 by (res_inst_tac [("n","m")] induct 1);
 by (ALLGOALS (Asm_simp_tac));
 qed "add_Suc_right";
diff -r bde086cfa597 -r e925308df78b src/FOL/ex/Nat2.ML
--- a/src/FOL/ex/Nat2.ML	Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/Nat2.ML	Thu Jun 18 18:28:45 1998 +0200
@@ -21,91 +21,91 @@
 by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
 qed "nat_exh";
 
-goal Nat2.thy "~ n=succ(n)";
+Goal "~ n=succ(n)";
 by (IND_TAC nat_ind Simp_tac "n" 1);
 result();
 
-goal Nat2.thy "~ succ(n)=n";
+Goal "~ succ(n)=n";
 by (IND_TAC nat_ind Simp_tac "n" 1);
 result();
 
-goal Nat2.thy "~ succ(succ(n))=n";
+Goal "~ succ(succ(n))=n";
 by (IND_TAC nat_ind Simp_tac "n" 1);
 result();
 
-goal Nat2.thy "~ n=succ(succ(n))";
+Goal "~ n=succ(succ(n))";
 by (IND_TAC nat_ind Simp_tac "n" 1);
 result();
 
-goal Nat2.thy "m+0 = m";
+Goal "m+0 = m";
 by (IND_TAC nat_ind Simp_tac "m" 1);
 qed "plus_0_right";
 
-goal Nat2.thy "m+succ(n) = succ(m+n)";
+Goal "m+succ(n) = succ(m+n)";
 by (IND_TAC nat_ind Simp_tac "m" 1);
 qed "plus_succ_right";
 
 Addsimps [plus_0_right, plus_succ_right];
 
-goal Nat2.thy "~n=0 --> m+pred(n) = pred(m+n)";
+Goal "~n=0 --> m+pred(n) = pred(m+n)";
 by (IND_TAC nat_ind Simp_tac "n" 1);
 result();
 
-goal Nat2.thy "~n=0 --> succ(pred(n))=n";
+Goal "~n=0 --> succ(pred(n))=n";
 by (IND_TAC nat_ind Simp_tac "n" 1);
 result();
 
-goal Nat2.thy "m+n=0 <-> m=0 & n=0";
+Goal "m+n=0 <-> m=0 & n=0";
 by (IND_TAC nat_ind Simp_tac "m" 1);
 result();
 
-goal Nat2.thy "m <= n --> m <= succ(n)";
+Goal "m <= n --> m <= succ(n)";
 by (IND_TAC nat_ind Simp_tac "m" 1);
 by (rtac (impI RS allI) 1);
 by (ALL_IND_TAC nat_ind Simp_tac 1);
 by (Fast_tac 1);
 bind_thm("le_imp_le_succ", result() RS mp);
 
-goal Nat2.thy "n<succ(n)";
+Goal "n<succ(n)";
 by (IND_TAC nat_ind Simp_tac "n" 1);
 result();
 
-goal Nat2.thy "~ n<n";
+Goal "~ n<n";
 by (IND_TAC nat_ind Simp_tac "n" 1);
 result();
 
-goal Nat2.thy "m < n --> m < succ(n)";
+Goal "m < n --> m < succ(n)";
 by (IND_TAC nat_ind Simp_tac "m" 1);
 by (rtac (impI RS allI) 1);
 by (ALL_IND_TAC nat_ind Simp_tac 1);
 by (Fast_tac 1);
 result();
 
-goal Nat2.thy "m <= n --> m <= n+k";
+Goal "m <= n --> m <= n+k";
 by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_imp_le_succ]))
      "k" 1);
 qed "le_plus";
 
-goal Nat2.thy "succ(m) <= n --> m <= n";
+Goal "succ(m) <= n --> m <= n";
 by (res_inst_tac [("x","n")]spec 1);
 by (ALL_IND_TAC nat_exh (simp_tac (simpset() addsimps [le_imp_le_succ])) 1);
 qed "succ_le";
 
-goal Nat2.thy "~m<n <-> n<=m";
+Goal "~m<n <-> n<=m";
 by (IND_TAC nat_ind Simp_tac "n" 1);
 by (rtac (impI RS allI) 1);
 by (ALL_IND_TAC nat_ind Asm_simp_tac 1);
 qed "not_less";
 
-goal Nat2.thy "n<=m --> ~m<n";
+Goal "n<=m --> ~m<n";
 by (simp_tac (simpset() addsimps [not_less]) 1);
 qed "le_imp_not_less";
 
-goal Nat2.thy "m<n --> ~n<=m";
+Goal "m<n --> ~n<=m";
 by (cut_facts_tac [not_less] 1 THEN Fast_tac 1);
 qed "not_le";
 
-goal Nat2.thy "m+k<=n --> m<=n";
+Goal "m+k<=n --> m<=n";
 by (IND_TAC nat_ind (K all_tac) "k" 1);
 by (Simp_tac 1);
 by (rtac (impI RS allI) 1);
@@ -122,14 +122,14 @@
 by (ALL_IND_TAC nat_exh Simp_tac 1);
 qed "not0";
 
-goal Nat2.thy "a<=a' & b<=b' --> a+b<=a'+b'";
+Goal "a<=a' & b<=b' --> a+b<=a'+b'";
 by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_plus])) "b" 1);
 by (resolve_tac [impI RS allI] 1);
 by (resolve_tac [allI RS allI] 1);
 by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
 qed "plus_le_plus";
 
-goal Nat2.thy "i<=j --> j<=k --> i<=k";
+Goal "i<=j --> j<=k --> i<=k";
 by (IND_TAC nat_ind (K all_tac) "i" 1);
 by (Simp_tac 1);
 by (resolve_tac [impI RS allI] 1);
@@ -139,7 +139,7 @@
 by (Fast_tac 1);
 qed "le_trans";
 
-goal Nat2.thy "i < j --> j <=k --> i < k";
+Goal "i < j --> j <=k --> i < k";
 by (IND_TAC nat_ind (K all_tac) "j" 1);
 by (Simp_tac 1);
 by (resolve_tac [impI RS allI] 1);
@@ -149,13 +149,13 @@
 by (Fast_tac 1);
 qed "less_le_trans";
 
-goal Nat2.thy "succ(i) <= j <-> i < j";
+Goal "succ(i) <= j <-> i < j";
 by (IND_TAC nat_ind Simp_tac "j" 1);
 by (resolve_tac [impI RS allI] 1);
 by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
 qed "succ_le2";
 
-goal Nat2.thy "i<succ(j) <-> i=j | i<j";
+Goal "i<succ(j) <-> i=j | i<j";
 by (IND_TAC nat_ind Simp_tac "j" 1);
 by (ALL_IND_TAC nat_exh Simp_tac 1);
 by (resolve_tac [impI RS allI] 1);
diff -r bde086cfa597 -r e925308df78b src/FOL/ex/NatClass.ML
--- a/src/FOL/ex/NatClass.ML	Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/NatClass.ML	Thu Jun 18 18:28:45 1998 +0200
@@ -7,7 +7,7 @@
 
 open NatClass;
 
-goal NatClass.thy "Suc(k) ~= (k::'a::nat)";
+Goal "Suc(k) ~= (k::'a::nat)";
 by (res_inst_tac [("n","k")] induct 1);
 by (rtac notI 1);
 by (etac Suc_neq_0 1);
@@ -17,7 +17,7 @@
 qed "Suc_n_not_n";
 
 
-goal NatClass.thy "(k+m)+n = k+(m+n)";
+Goal "(k+m)+n = k+(m+n)";
 prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
 by (rtac induct 1);
 back();
@@ -27,29 +27,29 @@
 back();
 back();
 
-goalw NatClass.thy [add_def] "0+n = n";
+Goalw [add_def] "0+n = n";
 by (rtac rec_0 1);
 qed "add_0";
 
-goalw NatClass.thy [add_def] "Suc(m)+n = Suc(m+n)";
+Goalw [add_def] "Suc(m)+n = Suc(m+n)";
 by (rtac rec_Suc 1);
 qed "add_Suc";
 
 Addsimps [add_0, add_Suc];
 
-goal NatClass.thy "(k+m)+n = k+(m+n)";
+Goal "(k+m)+n = k+(m+n)";
 by (res_inst_tac [("n","k")] induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "add_assoc";
 
-goal NatClass.thy "m+0 = m";
+Goal "m+0 = m";
 by (res_inst_tac [("n","m")] induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "add_0_right";
 
-goal NatClass.thy "m+Suc(n) = Suc(m+n)";
+Goal "m+Suc(n) = Suc(m+n)";
 by (res_inst_tac [("n","m")] induct 1);
 by (ALLGOALS (Asm_simp_tac));
 qed "add_Suc_right";
diff -r bde086cfa597 -r e925308df78b src/FOL/ex/Prolog.ML
--- a/src/FOL/ex/Prolog.ML	Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/Prolog.ML	Thu Jun 18 18:28:45 1998 +0200
@@ -8,19 +8,19 @@
 
 open Prolog;
 
-goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)";
+Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
 by (resolve_tac [appNil,appCons] 1);
 by (resolve_tac [appNil,appCons] 1);
 by (resolve_tac [appNil,appCons] 1);
 by (resolve_tac [appNil,appCons] 1);
 prth (result());
 
-goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)";
+Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
 by (REPEAT (resolve_tac [appNil,appCons] 1));
 result();
 
 
-goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)";
+Goal "app(?x, ?y, a:b:c:d:Nil)";
 by (REPEAT (resolve_tac [appNil,appCons] 1));
 back();
 back();
@@ -32,16 +32,16 @@
 (*app([x1,...,xn], y, ?z) requires (n+1) inferences*)
 (*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)
 
-goal Prolog.thy "rev(a:b:c:d:Nil, ?x)";
+Goal "rev(a:b:c:d:Nil, ?x)";
 val rules = [appNil,appCons,revNil,revCons];
 by (REPEAT (resolve_tac rules 1));
 result();
 
-goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
+Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
 by (REPEAT (resolve_tac rules 1));
 result();
 
-goal Prolog.thy "rev(?x, a:b:c:Nil)";
+Goal "rev(?x, a:b:c:Nil)";
 by (REPEAT (resolve_tac rules 1)); (*does not solve it directly!*)
 back();
 back();
@@ -53,19 +53,19 @@
 by prolog_tac;
 result();
 
-goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
+Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
 by prolog_tac;
 result();
 
 (*rev([a..p], ?w) requires 153 inferences *)
-goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)";
+Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)";
 by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
 (*Poly/ML: 4 secs >> 38 lips*)
 result();
 
 (*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences;
   total inferences = 2 + 1 + 17 + 561 = 581*)
-goal Prolog.thy
+Goal
     "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)";
 by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
 (*Poly/ML: 29 secs >> 20 lips*)
diff -r bde086cfa597 -r e925308df78b src/FOL/ex/prop.ML
--- a/src/FOL/ex/prop.ML	Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/prop.ML	Thu Jun 18 18:28:45 1998 +0200
@@ -11,66 +11,66 @@
 
 
 writeln"commutative laws of & and | ";
-goal thy "P & Q  -->  Q & P";
+Goal "P & Q  -->  Q & P";
 by tac;
 result();
 
-goal thy "P | Q  -->  Q | P";
+Goal "P | Q  -->  Q | P";
 by tac;
 result();
 
 
 writeln"associative laws of & and | ";
-goal thy "(P & Q) & R  -->  P & (Q & R)";
+Goal "(P & Q) & R  -->  P & (Q & R)";
 by tac;
 result();
 
-goal thy "(P | Q) | R  -->  P | (Q | R)";
+Goal "(P | Q) | R  -->  P | (Q | R)";
 by tac;
 result();
 
 
 
 writeln"distributive laws of & and | ";
-goal thy "(P & Q) | R  --> (P | R) & (Q | R)";
+Goal "(P & Q) | R  --> (P | R) & (Q | R)";
 by tac;
 result();
 
-goal thy "(P | R) & (Q | R)  --> (P & Q) | R";
+Goal "(P | R) & (Q | R)  --> (P & Q) | R";
 by tac;
 result();
 
-goal thy "(P | Q) & R  --> (P & R) | (Q & R)";
+Goal "(P | Q) & R  --> (P & R) | (Q & R)";
 by tac;
 result();
 
 
-goal thy "(P & R) | (Q & R)  --> (P | Q) & R";
+Goal "(P & R) | (Q & R)  --> (P | Q) & R";
 by tac;
 result();
 
 
 writeln"Laws involving implication";
 
-goal thy "(P-->R) & (Q-->R) <-> (P|Q --> R)";
+Goal "(P-->R) & (Q-->R) <-> (P|Q --> R)";
 by tac;
 result();
 
 
-goal thy "(P & Q --> R) <-> (P--> (Q-->R))";
+Goal "(P & Q --> R) <-> (P--> (Q-->R))";
 by tac;
 result();
 
 
-goal thy "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
+Goal "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
 by tac;
 result();
 
-goal thy "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
+Goal "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
 by tac;
 result();
 
-goal thy "(P --> Q & R) <-> (P-->Q)  &  (P-->R)";
+Goal "(P --> Q & R) <-> (P-->Q)  &  (P-->R)";
 by tac;
 result();
 
@@ -78,22 +78,22 @@
 writeln"Propositions-as-types";
 
 (*The combinator K*)
-goal thy "P --> (Q --> P)";
+Goal "P --> (Q --> P)";
 by tac;
 result();
 
 (*The combinator S*)
-goal thy "(P-->Q-->R)  --> (P-->Q) --> (P-->R)";
+Goal "(P-->Q-->R)  --> (P-->Q) --> (P-->R)";
 by tac;
 result();
 
 
 (*Converse is classical*)
-goal thy "(P-->Q) | (P-->R)  -->  (P --> Q | R)";
+Goal "(P-->Q) | (P-->R)  -->  (P --> Q | R)";
 by tac;
 result();
 
-goal thy "(P-->Q)  -->  (~Q --> ~P)";
+Goal "(P-->Q)  -->  (~Q --> ~P)";
 by tac;
 result();
 
@@ -101,39 +101,39 @@
 writeln"Schwichtenberg's examples (via T. Nipkow)";
 
 (* stab-imp *)
-goal thy "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
+Goal "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
 by tac;
 result();
 
 (* stab-to-peirce *)
-goal thy "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
+Goal "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
 \             --> ((P --> Q) --> P) --> P";
 by tac;
 result();
 
 (* peirce-imp1 *)
-goal thy "(((Q --> R) --> Q) --> Q) \
+Goal "(((Q --> R) --> Q) --> Q) \
 \              --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
 by tac;
 result();
   
 (* peirce-imp2 *)
-goal thy "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
+Goal "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
 by tac;
 result();
 
 (* mints  *)
-goal thy "((((P --> Q) --> P) --> P) --> Q) --> Q";
+Goal "((((P --> Q) --> P) --> P) --> Q) --> Q";
 by tac;
 result();
 
 (* mints-solovev *)
-goal thy "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
+Goal "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
 by tac;
 result();
 
 (* tatsuta *)
-goal thy "(((P7 --> P1) --> P10) --> P4 --> P5) \
+Goal "(((P7 --> P1) --> P10) --> P4 --> P5) \
 \         --> (((P8 --> P2) --> P9) --> P3 --> P10) \
 \         --> (P1 --> P8) --> P6 --> P7 \
 \         --> (((P3 --> P2) --> P9) --> P4) \
@@ -142,7 +142,7 @@
 result();
 
 (* tatsuta1 *)
-goal thy "(((P8 --> P2) --> P9) --> P3 --> P10) \
+Goal "(((P8 --> P2) --> P9) --> P3 --> P10) \
 \    --> (((P3 --> P2) --> P9) --> P4) \
 \    --> (((P6 --> P1) --> P2) --> P9) \
 \    --> (((P7 --> P1) --> P10) --> P4 --> P5) \
diff -r bde086cfa597 -r e925308df78b src/FOL/ex/quant.ML
--- a/src/FOL/ex/quant.ML	Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/quant.ML	Thu Jun 18 18:28:45 1998 +0200
@@ -9,73 +9,73 @@
 
 writeln"File FOL/ex/quant.";
 
-goal thy "(ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
+Goal "(ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
 by tac;
 result();  
 
 
-goal thy "(EX x y. P(x,y)) --> (EX y x. P(x,y))";
+Goal "(EX x y. P(x,y)) --> (EX y x. P(x,y))";
 by tac;
 result();  
 
 
 (*Converse is false*)
-goal thy "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
+Goal "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
 by tac;
 result();  
 
-goal thy "(ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
+Goal "(ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
 by tac;
 result();  
 
 
-goal thy "(ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
+Goal "(ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
 by tac;
 result();  
 
 
 writeln"Some harder ones";
 
-goal thy "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
+Goal "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
 by tac;
 result();  
 (*6 secs*)
 
 (*Converse is false*)
-goal thy "(EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
+Goal "(EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
 by tac;
 result();  
 
 
 writeln"Basic test of quantifier reasoning";
 (*TRUE*)
-goal thy "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
+Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
 by tac;  
 result();  
 
 
-goal thy "(ALL x. Q(x))  -->  (EX x. Q(x))";
+Goal "(ALL x. Q(x))  -->  (EX x. Q(x))";
 by tac;  
 result();  
 
 
 writeln"The following should fail, as they are false!";
 
-goal thy "(ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
+Goal "(ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
 by tac handle ERROR => writeln"Failed, as expected";  
 (*Check that subgoals remain: proof failed.*)
 getgoal 1; 
 
-goal thy "(EX x. Q(x))  -->  (ALL x. Q(x))";
+Goal "(EX x. Q(x))  -->  (ALL x. Q(x))";
 by tac handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
-goal thy "P(?a) --> (ALL x. P(x))";
+Goal "P(?a) --> (ALL x. P(x))";
 by tac handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
 getgoal 1;  
 
-goal thy
+Goal
     "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
 by tac handle ERROR => writeln"Failed, as expected";
 getgoal 1;  
@@ -83,23 +83,23 @@
 
 writeln"Back to things that are provable...";
 
-goal thy "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
+Goal "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
 by tac;  
 result();  
 
 
 (*An example of why exI should be delayed as long as possible*)
-goal thy "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
+Goal "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
 by tac;  
 result();  
 
-goal thy "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
+Goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
 by tac; 
 (*Verify that no subgoals remain.*) 
 uresult();  
 
 
-goal thy "(ALL x. Q(x))  -->  (EX x. Q(x))";
+Goal "(ALL x. Q(x))  -->  (EX x. Q(x))";
 by tac;
 result();  
 
@@ -108,19 +108,19 @@
 
 
 (*Principia Mathematica *11.53  *)
-goal thy "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
+Goal "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
 by tac;
 result();  
 (*6 secs*)
 
 (*Principia Mathematica *11.55  *)
-goal thy "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
+Goal "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
 by tac;
 result();  
 (*9 secs*)
 
 (*Principia Mathematica *11.61  *)
-goal thy "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
+Goal "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
 by tac;
 result();  
 (*3 secs*)