# HG changeset patch
# User wenzelm
# Date 898521482 -7200
# Node ID fbdb0b5413145b96ed516dd072316c9099a52509
# Parent  f947332d5465eec4307546b128e890389bc6ad39
isatool fixgoal;

diff -r f947332d5465 -r fbdb0b541314 src/CCL/CCL.ML
--- a/src/CCL/CCL.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/CCL.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -22,7 +22,7 @@
 qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
 
-goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
+Goal  "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
 by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
 by (fast_tac (set_cs addIs [po_abstractn]) 1);
 bind_thm("abstractn", standard (allI RS (result() RS mp)));
@@ -42,11 +42,11 @@
 
 (*** Termination and Divergence ***)
 
-goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
+Goalw [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
 by (rtac iff_refl 1);
 qed "Trm_iff";
 
-goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
+Goalw [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
 by (rtac iff_refl 1);
 qed "Dvg_iff";
 
@@ -140,13 +140,13 @@
 by (resolve_tac (prems RL [major RS ssubst]) 1);
 qed "XHlemma1";
 
-goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> &  P(t,t')} <-> Q)";
+Goal "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> &  P(t,t')} <-> Q)";
 by (fast_tac ccl_cs 1);
 bind_thm("XHlemma2", result() RS mp);
 
 (*** Pre-Order ***)
 
-goalw CCL.thy [POgen_def,SIM_def]  "mono(%X. POgen(X))";
+Goalw [POgen_def,SIM_def]  "mono(%X. POgen(X))";
 by (rtac monoI 1);
 by (safe_tac ccl_cs);
 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
@@ -154,14 +154,14 @@
 by (ALLGOALS (fast_tac set_cs));
 qed "POgen_mono";
 
-goalw CCL.thy [POgen_def,SIM_def]
+Goalw [POgen_def,SIM_def]
  "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
 \          (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
 \          (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))";
 by (rtac (iff_refl RS XHlemma2) 1);
 qed "POgenXH";
 
-goal CCL.thy
+Goal
   "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
 \                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
 \                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
@@ -171,24 +171,24 @@
 by (rtac (iff_refl RS XHlemma2) 1);
 qed "poXH";
 
-goal CCL.thy "bot [= b";
+Goal "bot [= b";
 by (rtac (poXH RS iffD2) 1);
 by (simp_tac ccl_ss 1);
 qed "po_bot";
 
-goal CCL.thy "a [= bot --> a=bot";
+Goal "a [= bot --> a=bot";
 by (rtac impI 1);
 by (dtac (poXH RS iffD1) 1);
 by (etac rev_mp 1);
 by (simp_tac ccl_ss 1);
 bind_thm("bot_poleast", result() RS mp);
 
-goal CCL.thy "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
+Goal "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
 by (rtac (poXH RS iff_trans) 1);
 by (simp_tac ccl_ss 1);
 qed "po_pair";
 
-goal CCL.thy "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
+Goal "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
 by (rtac (poXH RS iff_trans) 1);
 by (simp_tac ccl_ss 1);
 by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
@@ -229,14 +229,14 @@
 by (resolve_tac prems 1);
 qed "po_lemma";
 
-goal CCL.thy "~ <a,b> [= lam x. f(x)";
+Goal "~ <a,b> [= lam x. f(x)";
 by (rtac notI 1);
 by (rtac (npo_lam_bot RS notE) 1);
 by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
 qed "npo_pair_lam";
 
-goal CCL.thy "~ lam x. f(x) [= <a,b>";
+Goal "~ lam x. f(x) [= <a,b>";
 by (rtac notI 1);
 by (rtac (npo_lam_bot RS notE) 1);
 by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
@@ -266,7 +266,7 @@
 
 (*************** EQUALITY *******************)
 
-goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X. EQgen(X))";
+Goalw [EQgen_def,SIM_def]  "mono(%X. EQgen(X))";
 by (rtac monoI 1);
 by (safe_tac set_cs);
 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
@@ -274,7 +274,7 @@
 by (ALLGOALS (fast_tac set_cs));
 qed "EQgen_mono";
 
-goalw CCL.thy [EQgen_def,SIM_def]
+Goalw [EQgen_def,SIM_def]
   "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
 \                                            (t=false & t'=false) | \
 \                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
@@ -282,7 +282,7 @@
 by (rtac (iff_refl RS XHlemma2) 1);
 qed "EQgenXH";
 
-goal CCL.thy
+Goal
   "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
 \                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
 \                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))";
@@ -313,12 +313,12 @@
 
 (*** Untyped Case Analysis and Other Facts ***)
 
-goalw CCL.thy [apply_def]  "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
+Goalw [apply_def]  "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
 by (safe_tac ccl_cs);
 by (simp_tac ccl_ss 1);
 bind_thm("cond_eta", result() RS mp);
 
-goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
+Goal "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
 by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
 by (fast_tac set_cs 1);
 qed "exhaustion";
diff -r f947332d5465 -r fbdb0b541314 src/CCL/Fix.ML
--- a/src/CCL/Fix.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Fix.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -44,7 +44,7 @@
 
 (*** Lemmas for Inclusive Predicates ***)
 
-goal Fix.thy "INCL(%x.~ a(x) [= t)";
+Goal "INCL(%x.~ a(x) [= t)";
 by (rtac inclI 1);
 by (dtac bspec 1);
 by (rtac zeroT 1);
@@ -67,7 +67,7 @@
 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
 qed "ball_INCL";
 
-goal Fix.thy "INCL(%x. a(x) = (b(x)::'a::prog))";
+Goal "INCL(%x. a(x) = (b(x)::'a::prog))";
 by (simp_tac (term_ss addsimps [eq_iff]) 1);
 by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
 qed "eq_INCL";
@@ -76,11 +76,11 @@
 
 (* Fixed points of idgen *)
 
-goal Fix.thy "idgen(fix(idgen)) = fix(idgen)";
+Goal "idgen(fix(idgen)) = fix(idgen)";
 by (rtac (fixB RS sym) 1);
 qed "fix_idgenfp";
 
-goalw Fix.thy [idgen_def] "idgen(lam x. x) = lam x. x";
+Goalw [idgen_def] "idgen(lam x. x) = lam x. x";
 by (simp_tac term_ss 1);
 by (rtac (term_case RS allI) 1);
 by (ALLGOALS (simp_tac term_ss));
@@ -161,7 +161,7 @@
 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
 qed "id_least_idgen";
 
-goal Fix.thy  "fix(idgen) = lam x. x";
+Goal  "fix(idgen) = lam x. x";
 by (fast_tac (term_cs addIs [eq_iff RS iffD2,
                              id_idgenfp RS fix_least_idgen,
                              fix_idgenfp RS id_least_idgen]) 1);
diff -r f947332d5465 -r fbdb0b541314 src/CCL/Hered.ML
--- a/src/CCL/Hered.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Hered.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -12,18 +12,18 @@
 
 (*** Hereditary Termination ***)
 
-goalw Hered.thy [HTTgen_def]  "mono(%X. HTTgen(X))";
+Goalw [HTTgen_def]  "mono(%X. HTTgen(X))";
 by (rtac monoI 1);
 by (fast_tac set_cs 1);
 qed "HTTgen_mono";
 
-goalw Hered.thy [HTTgen_def]
+Goalw [HTTgen_def]
   "t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) | \
 \                                       (EX f. t=lam x. f(x) & (ALL x. f(x) : A))";
 by (fast_tac set_cs 1);
 qed "HTTgenXH";
 
-goal Hered.thy
+Goal
   "t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \
 \                                  (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))";
 by (rtac (rewrite_rule [HTTgen_def] 
@@ -33,24 +33,24 @@
 
 (*** Introduction Rules for HTT ***)
 
-goal Hered.thy "~ bot : HTT";
+Goal "~ bot : HTT";
 by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
 qed "HTT_bot";
 
-goal Hered.thy "true : HTT";
+Goal "true : HTT";
 by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
 qed "HTT_true";
 
-goal Hered.thy "false : HTT";
+Goal "false : HTT";
 by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
 qed "HTT_false";
 
-goal Hered.thy "<a,b> : HTT <->  a : HTT  & b : HTT";
+Goal "<a,b> : HTT <->  a : HTT  & b : HTT";
 by (rtac (HTTXH RS iff_trans) 1);
 by (fast_tac term_cs 1);
 qed "HTT_pair";
 
-goal Hered.thy "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)";
+Goal "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)";
 by (rtac (HTTXH RS iff_trans) 1);
 by (simp_tac term_ss 1);
 by (safe_tac term_cs);
@@ -112,11 +112,11 @@
 
 (*** Formation Rules for Types ***)
 
-goal Hered.thy "Unit <= HTT";
+Goal "Unit <= HTT";
 by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
 qed "UnitF";
 
-goal Hered.thy "Bool <= HTT";
+Goal "Bool <= HTT";
 by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1);
 by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
 qed "BoolF";
@@ -136,14 +136,14 @@
 (***                                          exhaution rule for type-former ***)
 
 (*Proof by induction - needs induction rule for type*)
-goal Hered.thy "Nat <= HTT";
+Goal "Nat <= HTT";
 by (simp_tac (term_ss addsimps [subsetXH]) 1);
 by (safe_tac set_cs);
 by (etac Nat_ind 1);
 by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD]))));
 val NatF = result();
 
-goal Hered.thy "Nat <= HTT";
+Goal "Nat <= HTT";
 by (safe_tac set_cs);
 by (etac HTT_coinduct3 1);
 by (fast_tac (set_cs addIs HTTgenIs 
diff -r f947332d5465 -r fbdb0b541314 src/CCL/Set.ML
--- a/src/CCL/Set.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Set.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -116,7 +116,7 @@
 qed_goal "subset_refl" Set.thy "A <= A"
  (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
 
-goal Set.thy "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
+Goal "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
 by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
 qed "subset_trans";
@@ -163,7 +163,7 @@
 by (REPEAT (resolve_tac (refl::prems) 1));
 qed "setup_induction";
 
-goal Set.thy "{x. x:A} = A";
+Goal "{x. x:A} = A";
 by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1  ORELSE etac CollectD 1));
 qed "trivial_set";
 
@@ -234,7 +234,7 @@
 
 (*** Empty sets ***)
 
-goalw Set.thy [empty_def] "{x. False} = {}";
+Goalw [empty_def] "{x. False} = {}";
 by (rtac refl 1);
 qed "empty_eq";
 
@@ -252,7 +252,7 @@
 
 (*** Singleton sets ***)
 
-goalw Set.thy [singleton_def] "a : {a}";
+Goalw [singleton_def] "a : {a}";
 by (rtac CollectI 1);
 by (rtac refl 1);
 qed "singletonI";
diff -r f947332d5465 -r fbdb0b541314 src/CCL/Term.ML
--- a/src/CCL/Term.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Term.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -21,33 +21,33 @@
 
 (*** Beta Rules, including strictness ***)
 
-goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
+Goalw [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
 by (res_inst_tac [("t","t")] term_case 1);
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
 bind_thm("letB", result() RS mp);
 
-goalw Term.thy [let_def] "let x be bot in f(x) = bot";
+Goalw [let_def] "let x be bot in f(x) = bot";
 by (rtac caseBbot 1);
 qed "letBabot";
 
-goalw Term.thy [let_def] "let x be t in bot = bot";
+Goalw [let_def] "let x be t in bot = bot";
 by (resolve_tac ([caseBbot] RL [term_case]) 1);
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
 qed "letBbbot";
 
-goalw Term.thy [apply_def] "(lam x. b(x)) ` a = b(a)";
+Goalw [apply_def] "(lam x. b(x)) ` a = b(a)";
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
 qed "applyB";
 
-goalw Term.thy [apply_def] "bot ` a = bot";
+Goalw [apply_def] "bot ` a = bot";
 by (rtac caseBbot 1);
 qed "applyBbot";
 
-goalw Term.thy [fix_def] "fix(f) = f(fix(f))";
+Goalw [fix_def] "fix(f) = f(fix(f))";
 by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
 qed "fixB";
 
-goalw Term.thy [letrec_def]
+Goalw [letrec_def]
       "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))";
 by (resolve_tac [fixB RS ssubst] 1 THEN 
     resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
diff -r f947332d5465 -r fbdb0b541314 src/CCL/Trancl.ML
--- a/src/CCL/Trancl.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Trancl.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -27,7 +27,7 @@
 
 (** Identity relation **)
 
-goalw Trancl.thy [id_def] "<a,a> : id";  
+Goalw [id_def] "<a,a> : id";  
 by (rtac CollectI 1);
 by (rtac exI 1);
 by (rtac refl 1);
@@ -77,7 +77,7 @@
 
 (** The relation rtrancl **)
 
-goal Trancl.thy "mono(%s. id Un (r O s))";
+Goal "mono(%s. id Un (r O s))";
 by (rtac monoI 1);
 by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
 qed "rtrancl_fun_mono";
@@ -85,7 +85,7 @@
 val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);
 
 (*Reflexivity of rtrancl*)
-goal Trancl.thy "<a,a> : r^*";
+Goal "<a,a> : r^*";
 by (stac rtrancl_unfold 1);
 by (fast_tac comp_cs 1);
 qed "rtrancl_refl";
@@ -133,7 +133,7 @@
 qed "rtrancl_induct";
 
 (*transitivity of transitive closure!! -- by induction.*)
-goal Trancl.thy "trans(r^*)";
+Goal "trans(r^*)";
 by (rtac transI 1);
 by (res_inst_tac [("b","z")] rtrancl_induct 1);
 by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1));
@@ -200,7 +200,7 @@
 
 (*Transitivity of r^+.
   Proved by unfolding since it uses transitivity of rtrancl. *)
-goalw Trancl.thy [trancl_def] "trans(r^+)";
+Goalw [trancl_def] "trans(r^+)";
 by (rtac transI 1);
 by (REPEAT (etac compEpair 1));
 by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1);
diff -r f947332d5465 -r fbdb0b541314 src/CCL/Type.ML
--- a/src/CCL/Type.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Type.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -108,11 +108,11 @@
 
 (*** Monotonicity ***)
 
-goal Type.thy "mono (%X. X)";
+Goal "mono (%X. X)";
 by (REPEAT (ares_tac [monoI] 1));
 qed "idM";
 
-goal Type.thy "mono(%X. A)";
+Goal "mono(%X. A)";
 by (REPEAT (ares_tac [monoI,subset_refl] 1));
 qed "constM";
 
@@ -156,18 +156,18 @@
 
 (*** Conversion Rules for Fixed Points via monotonicity and Tarski ***)
 
-goal Type.thy "mono(%X. Unit+X)";
+Goal "mono(%X. Unit+X)";
 by (REPEAT (ares_tac [PlusM,constM,idM] 1));
 qed "NatM";
 bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
 
-goal Type.thy "mono(%X.(Unit+Sigma(A,%y. X)))";
+Goal "mono(%X.(Unit+Sigma(A,%y. X)))";
 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
 qed "ListM";
 bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
 bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
 
-goal Type.thy "mono(%X.({} + Sigma(A,%y. X)))";
+Goal "mono(%X.({} + Sigma(A,%y. X)))";
 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
 qed "IListsM";
 bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
diff -r f947332d5465 -r fbdb0b541314 src/CCL/Wfd.ML
--- a/src/CCL/Wfd.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Wfd.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -63,7 +63,7 @@
 
 (*** Lexicographic Ordering ***)
 
-goalw Wfd.thy [lex_def] 
+Goalw [lex_def] 
  "p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
 by (fast_tac ccl_cs 1);
 qed "lexXH";
@@ -109,7 +109,7 @@
 
 (*** Mapping ***)
 
-goalw Wfd.thy [wmap_def] 
+Goalw [wmap_def] 
  "p : wmap(f,r) <-> (EX x y. p=<x,y>  &  <f(x),f(y)> : r)";
 by (fast_tac ccl_cs 1);
 qed "wmapXH";
@@ -175,18 +175,18 @@
 by (rtac Empty_wf 1);
 qed "wf_wf";
 
-goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)";
+Goalw [NatPR_def]  "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)";
 by (fast_tac set_cs 1);
 qed "NatPRXH";
 
-goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)";
+Goalw [ListPR_def]  "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)";
 by (fast_tac set_cs 1);
 qed "ListPRXH";
 
 val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2));
 val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2)));
 
-goalw Wfd.thy [Wfd_def]  "Wfd(NatPR)";
+Goalw [Wfd_def]  "Wfd(NatPR)";
 by (safe_tac set_cs);
 by (wfd_strengthen_tac "%x. x:Nat" 1);
 by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
@@ -194,7 +194,7 @@
 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
 qed "NatPR_wf";
 
-goalw Wfd.thy [Wfd_def]  "Wfd(ListPR(A))";
+Goalw [Wfd_def]  "Wfd(ListPR(A))";
 by (safe_tac set_cs);
 by (wfd_strengthen_tac "%x. x:List(A)" 1);
 by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
diff -r f947332d5465 -r fbdb0b541314 src/CCL/ex/Stream.ML
--- a/src/CCL/ex/Stream.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/ex/Stream.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -84,12 +84,12 @@
 (*        fun iter1(f,a) = a$iter1(f,f(a))                            *)
 (*        fun iter2(f,a) = a$map(f,iter2(f,a))                        *)
 
-goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
+Goalw [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
 by (rtac (letrecB RS trans) 1);
 by (simp_tac term_ss 1);
 qed "iter1B";
 
-goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
+Goalw [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
 by (rtac (letrecB RS trans) 1);
 by (rtac refl 1);
 qed "iter2B";
@@ -101,7 +101,7 @@
 by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
 qed "iter2Blemma";
 
-goal Stream.thy "iter1(f,a) = iter2(f,a)";
+Goal "iter1(f,a) = iter2(f,a)";
 by (eq_coinduct3_tac 
     "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
     1);