1.1 --- a/src/ZF/AC/WO6_WO1.ML Wed Mar 22 12:33:34 2000 +0100
1.2 +++ b/src/ZF/AC/WO6_WO1.ML Wed Mar 22 12:45:41 2000 +0100
1.3 @@ -113,11 +113,10 @@
1.4 by (REPEAT (fast_tac (claset() addSEs [LeastI]) 1));
1.5 qed "nested_LeastI";
1.6
1.7 -val nested_Least_instance =
1.8 - standard
1.9 - (read_instantiate
1.10 - [("P","%g d. domain(uu(f,b,g,d)) ~= 0 & \
1.11 -\ domain(uu(f,b,g,d)) lepoll m")] nested_LeastI);
1.12 +bind_thm ("nested_Least_instance",
1.13 + inst "P"
1.14 + "%g d. domain(uu(f,b,g,d)) ~= 0 & domain(uu(f,b,g,d)) lepoll m"
1.15 + nested_LeastI);
1.16
1.17 Goalw [gg1_def]
1.18 "!!a. [| Ord(a); m:nat; \
2.1 --- a/src/ZF/Arith.ML Wed Mar 22 12:33:34 2000 +0100
2.2 +++ b/src/ZF/Arith.ML Wed Mar 22 12:45:41 2000 +0100
2.3 @@ -246,8 +246,8 @@
2.4 qed "diff_cancel";
2.5
2.6 Goal "[| k:nat; m: nat; n: nat |] ==> (m#+k) #- (n#+k) = m #- n";
2.7 -val add_commute_k = read_instantiate [("n","k")] add_commute;
2.8 -by (asm_simp_tac (simpset() addsimps [add_commute_k, diff_cancel]) 1);
2.9 +by (asm_simp_tac
2.10 + (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
2.11 qed "diff_cancel2";
2.12
2.13 Goal "[| m:nat; n:nat |] ==> n #- (n#+m) = 0";
2.14 @@ -263,9 +263,8 @@
2.15 qed "diff_mult_distrib" ;
2.16
2.17 Goal "[| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)";
2.18 -val mult_commute_k = read_instantiate [("m","k")] mult_commute;
2.19 -by (asm_simp_tac (simpset() addsimps
2.20 - [mult_commute_k, diff_mult_distrib]) 1);
2.21 +by (asm_simp_tac
2.22 + (simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
2.23 qed "diff_mult_distrib2" ;
2.24
2.25 (*** Remainder ***)
3.1 --- a/src/ZF/CardinalArith.ML Wed Mar 22 12:33:34 2000 +0100
3.2 +++ b/src/ZF/CardinalArith.ML Wed Mar 22 12:45:41 2000 +0100
3.3 @@ -291,7 +291,7 @@
3.4 Goal "Card(n) ==> 2 |*| n = n |+| n";
3.5 by (asm_simp_tac
3.6 (simpset() addsimps [cmult_succ_lemma, Card_is_Ord,
3.7 - read_instantiate [("j","0")] cadd_commute]) 1);
3.8 + inst "j" "0" cadd_commute]) 1);
3.9 qed "cmult_2";
3.10
3.11
4.1 --- a/src/ZF/Ordinal.ML Wed Mar 22 12:33:34 2000 +0100
4.2 +++ b/src/ZF/Ordinal.ML Wed Mar 22 12:45:41 2000 +0100
4.3 @@ -573,8 +573,7 @@
4.4
4.5 val [ordi,ordj,ordk] = goal Ordinal.thy
4.6 "[| Ord(i); Ord(j); Ord(k) |] ==> i Un j : k <-> i:k & j:k";
4.7 -by (cut_facts_tac [[ordi,ordj] MRS
4.8 - read_instantiate [("k","k")] Un_least_lt_iff] 1);
4.9 +by (cut_inst_tac [("k","k")] ([ordi,ordj] MRS Un_least_lt_iff) 1);
4.10 by (asm_full_simp_tac (simpset() addsimps [lt_def,ordi,ordj,ordk]) 1);
4.11 qed "Un_least_mem_iff";
4.12
5.1 --- a/src/ZF/Perm.ML Wed Mar 22 12:33:34 2000 +0100
5.2 +++ b/src/ZF/Perm.ML Wed Mar 22 12:45:41 2000 +0100
5.3 @@ -245,7 +245,7 @@
5.4 bind_thm ("compEpair",
5.5 rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
5.6 THEN prune_params_tac)
5.7 - (read_instantiate [("xz","<a,c>")] compE));
5.8 + (inst "xz" "<a,c>" compE));
5.9
5.10 AddSIs [idI];
5.11 AddIs [compI];
6.1 --- a/src/ZF/QPair.ML Wed Mar 22 12:33:34 2000 +0100
6.2 +++ b/src/ZF/QPair.ML Wed Mar 22 12:45:41 2000 +0100
6.3 @@ -67,7 +67,7 @@
6.4 val QSigmaE2 =
6.5 rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
6.6 THEN prune_params_tac)
6.7 - (read_instantiate [("c","<a;b>")] QSigmaE);
6.8 + (inst "c" "<a;b>" QSigmaE);
6.9
6.10 qed_goal "QSigmaD1" thy "<a;b> : QSigma(A,B) ==> a : A"
6.11 (fn [major]=>
7.1 --- a/src/ZF/ex/Limit.ML Wed Mar 22 12:33:34 2000 +0100
7.2 +++ b/src/ZF/ex/Limit.ML Wed Mar 22 12:45:41 2000 +0100
7.3 @@ -1782,8 +1782,9 @@
7.4 by (etac leE 1);
7.5 by (asm_simp_tac(simpset() addsimps[e_less_eq,e_gr_eq]) 2);
7.6 (* Must control rewriting by instantiating a variable. *)
7.7 -by (asm_full_simp_tac(simpset() addsimps
7.8 - [read_instantiate [("i1","n")] (nat_into_Ord RS not_le_iff_lt RS iff_sym),
7.9 +by (asm_full_simp_tac
7.10 + (simpset() addsimps
7.11 + [inst "i1" "n" (nat_into_Ord RS not_le_iff_lt RS iff_sym),
7.12 add_le_self]) 1);
7.13 qed "eps_e_gr_add";
7.14
7.15 @@ -2488,8 +2489,9 @@
7.16 by (res_inst_tac[("b","t")](lub_const RS subst) 2);
7.17 by (stac comp_lubs 4);
7.18 by (asm_simp_tac (simpset() addsimps [comp_assoc,
7.19 - read_instantiate [("f","f")] mediating_eq]) 9);
7.20 -brr[cont_fun, emb_cont, mediating_emb, cont_cf, cpo_cf, chain_const, commute_chain,emb_chain_cpo] 1;
7.21 + inst "f" "f" mediating_eq]) 9);
7.22 +brr[cont_fun, emb_cont, mediating_emb, cont_cf, cpo_cf, chain_const,
7.23 + commute_chain,emb_chain_cpo] 1;
7.24 qed "lub_universal_unique";
7.25
7.26 (*---------------------------------------------------------------------*)
8.1 --- a/src/ZF/upair.ML Wed Mar 22 12:33:34 2000 +0100
8.2 +++ b/src/ZF/upair.ML Wed Mar 22 12:45:41 2000 +0100
8.3 @@ -272,11 +272,11 @@
8.4 addsplits[split_if]
8.5 **)
8.6
8.7 -bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
8.8 -bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
8.9 +bind_thm ("split_if_eq1", inst "P" "%x. x = ?b" split_if);
8.10 +bind_thm ("split_if_eq2", inst "P" "%x. ?a = x" split_if);
8.11
8.12 -bind_thm ("split_if_mem1", read_instantiate [("P", "%x. x : ?b")] split_if);
8.13 -bind_thm ("split_if_mem2", read_instantiate [("P", "%x. ?a : x")] split_if);
8.14 +bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
8.15 +bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if);
8.16
8.17 val split_ifs = [split_if_eq1, split_if_eq2,
8.18 split_if_mem1, split_if_mem2];