1.1 --- a/src/ZF/Induct/Primrec.thy Mon Feb 11 21:32:11 2008 +0100
1.2 +++ b/src/ZF/Induct/Primrec.thy Mon Feb 11 21:32:12 2008 +0100
1.3 @@ -31,7 +31,7 @@
1.4
1.5 definition
1.6 COMP :: "[i,i]=>i" where
1.7 - "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` List_ZF.map(\<lambda>f. f`l, fs)"
1.8 + "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` map(\<lambda>f. f`l, fs)"
1.9
1.10 definition
1.11 PREC :: "[i,i]=>i" where
1.12 @@ -93,7 +93,7 @@
1.13 monos list_mono
1.14 con_defs SC_def CONSTANT_def PROJ_def COMP_def PREC_def
1.15 type_intros nat_typechecks list.intros
1.16 - lam_type list_case_type drop_type List_ZF.map_type
1.17 + lam_type list_case_type drop_type map_type
1.18 apply_type rec_type
1.19
1.20
2.1 --- a/src/ZF/Induct/Term.thy Mon Feb 11 21:32:11 2008 +0100
2.2 +++ b/src/ZF/Induct/Term.thy Mon Feb 11 21:32:12 2008 +0100
2.3 @@ -235,7 +235,7 @@
2.4 \medskip Theorems about @{text term_map}.
2.5 *}
2.6
2.7 -declare List_ZF.map_compose [simp]
2.8 +declare map_compose [simp]
2.9
2.10 lemma term_map_ident: "t \<in> term(A) ==> term_map(\<lambda>u. u, t) = t"
2.11 by (induct rule: term_induct_eqn) simp
3.1 --- a/src/ZF/UNITY/Monotonicity.thy Mon Feb 11 21:32:11 2008 +0100
3.2 +++ b/src/ZF/UNITY/Monotonicity.thy Mon Feb 11 21:32:12 2008 +0100
3.3 @@ -69,7 +69,7 @@
3.4 lemma take_mono_left:
3.5 "[| i le j; xs \<in> list(A); j \<in> nat |]
3.6 ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
3.7 -by (blast intro: Nat_ZF.le_in_nat take_mono_left_lemma)
3.8 +by (blast intro: le_in_nat take_mono_left_lemma)
3.9
3.10 lemma take_mono_right:
3.11 "[| <xs,ys> \<in> prefix(A); i \<in> nat |]
4.1 --- a/src/ZF/ind_syntax.ML Mon Feb 11 21:32:11 2008 +0100
4.2 +++ b/src/ZF/ind_syntax.ML Mon Feb 11 21:32:12 2008 +0100
4.3 @@ -127,7 +127,7 @@
4.4 (fn t => "Datatype set not previously declared as constant: " ^
4.5 Sign.string_of_term @{theory IFOL} t);
4.6 val rec_names = (*nat doesn't have to be added*)
4.7 - @{const_name "Nat_ZF.nat"} :: map (#1 o dest_Const) rec_hds
4.8 + @{const_name "nat"} :: map (#1 o dest_Const) rec_hds
4.9 val u = if co then quniv else univ
4.10 val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
4.11 (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
5.1 --- a/src/ZF/int_arith.ML Mon Feb 11 21:32:11 2008 +0100
5.2 +++ b/src/ZF/int_arith.ML Mon Feb 11 21:32:12 2008 +0100
5.3 @@ -111,11 +111,11 @@
5.4 | find_first_numeral past [] = raise TERM("find_first_numeral", []);
5.5
5.6 val zero = mk_numeral 0;
5.7 -val mk_plus = FOLogic.mk_binop @{const_name "Int_ZF.zadd"};
5.8 +val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
5.9
5.10 val iT = Ind_Syntax.iT;
5.11
5.12 -val zminus_const = Const (@{const_name "Int_ZF.zminus"}, iT --> iT);
5.13 +val zminus_const = Const (@{const_name "zminus"}, iT --> iT);
5.14
5.15 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
5.16 fun mk_sum [] = zero
5.17 @@ -126,30 +126,30 @@
5.18 fun long_mk_sum [] = zero
5.19 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
5.20
5.21 -val dest_plus = FOLogic.dest_bin @{const_name "Int_ZF.zadd"} iT;
5.22 +val dest_plus = FOLogic.dest_bin @{const_name "zadd"} iT;
5.23
5.24 (*decompose additions AND subtractions as a sum*)
5.25 -fun dest_summing (pos, Const (@{const_name "Int_ZF.zadd"}, _) $ t $ u, ts) =
5.26 +fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
5.27 dest_summing (pos, t, dest_summing (pos, u, ts))
5.28 - | dest_summing (pos, Const (@{const_name "Int_ZF.zdiff"}, _) $ t $ u, ts) =
5.29 + | dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) =
5.30 dest_summing (pos, t, dest_summing (not pos, u, ts))
5.31 | dest_summing (pos, t, ts) =
5.32 if pos then t::ts else zminus_const$t :: ts;
5.33
5.34 fun dest_sum t = dest_summing (true, t, []);
5.35
5.36 -val mk_diff = FOLogic.mk_binop @{const_name "Int_ZF.zdiff"};
5.37 -val dest_diff = FOLogic.dest_bin @{const_name "Int_ZF.zdiff"} iT;
5.38 +val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
5.39 +val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} iT;
5.40
5.41 val one = mk_numeral 1;
5.42 -val mk_times = FOLogic.mk_binop @{const_name "Int_ZF.zmult"};
5.43 +val mk_times = FOLogic.mk_binop @{const_name "zmult"};
5.44
5.45 fun mk_prod [] = one
5.46 | mk_prod [t] = t
5.47 | mk_prod (t :: ts) = if t = one then mk_prod ts
5.48 else mk_times (t, mk_prod ts);
5.49
5.50 -val dest_times = FOLogic.dest_bin @{const_name "Int_ZF.zmult"} iT;
5.51 +val dest_times = FOLogic.dest_bin @{const_name "zmult"} iT;
5.52
5.53 fun dest_prod t =
5.54 let val (t,u) = dest_times t
5.55 @@ -160,7 +160,7 @@
5.56 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
5.57
5.58 (*Express t as a product of (possibly) a numeral with other sorted terms*)
5.59 -fun dest_coeff sign (Const (@{const_name "Int_ZF.zminus"}, _) $ t) = dest_coeff (~sign) t
5.60 +fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
5.61 | dest_coeff sign t =
5.62 let val ts = sort Term.term_ord (dest_prod t)
5.63 val (n, ts') = find_first_numeral [] ts
5.64 @@ -254,8 +254,8 @@
5.65 structure LessCancelNumerals = CancelNumeralsFun
5.66 (open CancelNumeralsCommon
5.67 val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
5.68 - val mk_bal = FOLogic.mk_binrel @{const_name "Int_ZF.zless"}
5.69 - val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zless"} iT
5.70 + val mk_bal = FOLogic.mk_binrel @{const_name "zless"}
5.71 + val dest_bal = FOLogic.dest_bin @{const_name "zless"} iT
5.72 val bal_add1 = less_add_iff1 RS iff_trans
5.73 val bal_add2 = less_add_iff2 RS iff_trans
5.74 );
5.75 @@ -263,8 +263,8 @@
5.76 structure LeCancelNumerals = CancelNumeralsFun
5.77 (open CancelNumeralsCommon
5.78 val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
5.79 - val mk_bal = FOLogic.mk_binrel @{const_name "Int_ZF.zle"}
5.80 - val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zle"} iT
5.81 + val mk_bal = FOLogic.mk_binrel @{const_name "zle"}
5.82 + val dest_bal = FOLogic.dest_bin @{const_name "zle"} iT
5.83 val bal_add1 = le_add_iff1 RS iff_trans
5.84 val bal_add2 = le_add_iff2 RS iff_trans
5.85 );