--- a/lib/Tools/build Wed May 07 12:25:35 2014 +0200
+++ b/lib/Tools/build Wed May 07 14:51:51 2014 +0200
@@ -144,7 +144,7 @@
"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
"$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
"$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
- "${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \
+ "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
"${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
RC="$?"
--- a/src/Doc/Implementation/Integration.thy Wed May 07 12:25:35 2014 +0200
+++ b/src/Doc/Implementation/Integration.thy Wed May 07 14:51:51 2014 +0200
@@ -133,7 +133,6 @@
text %mlref {*
\begin{mldecls}
- @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
@{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
Toplevel.transition -> Toplevel.transition"} \\
@{index_ML Toplevel.theory: "(theory -> theory) ->
@@ -150,10 +149,6 @@
\begin{description}
- \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
- causes the toplevel loop to echo the result state (in interactive
- mode).
-
\item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
function.
--- a/src/HOL/HOLCF/Tools/cpodef.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Wed May 07 14:51:51 2014 +0200
@@ -336,13 +336,11 @@
val _ =
Outer_Syntax.command @{command_spec "pcpodef"}
"HOLCF type definition (requires admissibility proof)"
- (typedef_proof_decl >>
- (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)))
+ (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
val _ =
Outer_Syntax.command @{command_spec "cpodef"}
"HOLCF type definition (requires admissibility proof)"
- (typedef_proof_decl >>
- (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)))
+ (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
end
--- a/src/HOL/HOLCF/Tools/domaindef.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Wed May 07 14:51:51 2014 +0200
@@ -212,7 +212,6 @@
val _ =
Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
- (domaindef_decl >>
- (Toplevel.print oo (Toplevel.theory o mk_domaindef)))
+ (domaindef_decl >> (Toplevel.theory o mk_domaindef))
end
--- a/src/HOL/Library/Set_Algebras.thy Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/Library/Set_Algebras.thy Wed May 07 14:51:51 2014 +0200
@@ -9,7 +9,7 @@
begin
text {*
- This library lifts operations like addition and muliplication to
+ This library lifts operations like addition and multiplication to
sets. It was designed to support asymptotic calculations. See the
comments at the top of theory @{text BigO}.
*}
@@ -38,17 +38,17 @@
begin
definition
- set_zero[simp]: "0::('a::zero)set == {0}"
+ set_zero[simp]: "(0::'a::zero set) = {0}"
instance ..
end
-
+
instantiation set :: (one) one
begin
definition
- set_one[simp]: "1::('a::one)set == {1}"
+ set_one[simp]: "(1::'a::one set) = {1}"
instance ..
@@ -64,30 +64,30 @@
"x =o A \<equiv> x \<in> A"
instance set :: (semigroup_add) semigroup_add
-by default (force simp add: set_plus_def add.assoc)
+ by default (force simp add: set_plus_def add.assoc)
instance set :: (ab_semigroup_add) ab_semigroup_add
-by default (force simp add: set_plus_def add.commute)
+ by default (force simp add: set_plus_def add.commute)
instance set :: (monoid_add) monoid_add
-by default (simp_all add: set_plus_def)
+ by default (simp_all add: set_plus_def)
instance set :: (comm_monoid_add) comm_monoid_add
-by default (simp_all add: set_plus_def)
+ by default (simp_all add: set_plus_def)
instance set :: (semigroup_mult) semigroup_mult
-by default (force simp add: set_times_def mult.assoc)
+ by default (force simp add: set_times_def mult.assoc)
instance set :: (ab_semigroup_mult) ab_semigroup_mult
-by default (force simp add: set_times_def mult.commute)
+ by default (force simp add: set_times_def mult.commute)
instance set :: (monoid_mult) monoid_mult
-by default (simp_all add: set_times_def)
+ by default (simp_all add: set_times_def)
instance set :: (comm_monoid_mult) comm_monoid_mult
-by default (simp_all add: set_times_def)
+ by default (simp_all add: set_times_def)
-lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
+lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
by (auto simp add: set_plus_def)
lemma set_plus_elim:
@@ -95,11 +95,11 @@
obtains a b where "x = a + b" and "a \<in> A" and "b \<in> B"
using assms unfolding set_plus_def by fast
-lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
+lemma set_plus_intro2 [intro]: "b \<in> C \<Longrightarrow> a + b \<in> a +o C"
by (auto simp add: elt_set_plus_def)
-lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
- (b +o D) = (a + b) +o (C + D)"
+lemma set_plus_rearrange:
+ "((a::'a::comm_monoid_add) +o C) + (b +o D) = (a + b) +o (C + D)"
apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
apply (rule_tac x = "ba + bb" in exI)
apply (auto simp add: add_ac)
@@ -107,12 +107,10 @@
apply (auto simp add: add_ac)
done
-lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
- (a + b) +o C"
+lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = (a + b) +o C"
by (auto simp add: elt_set_plus_def add_assoc)
-lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
- a +o (B + C)"
+lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = a +o (B + C)"
apply (auto simp add: elt_set_plus_def set_plus_def)
apply (blast intro: add_ac)
apply (rule_tac x = "a + aa" in exI)
@@ -123,8 +121,7 @@
apply (auto simp add: add_ac)
done
-theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
- a +o (C + D)"
+theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = a +o (C + D)"
apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
apply (rule_tac x = "aa + ba" in exI)
apply (auto simp add: add_ac)
@@ -133,48 +130,43 @@
theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
set_plus_rearrange3 set_plus_rearrange4
-lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
+lemma set_plus_mono [intro!]: "C \<subseteq> D \<Longrightarrow> a +o C \<subseteq> a +o D"
by (auto simp add: elt_set_plus_def)
-lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
- C + E <= D + F"
+lemma set_plus_mono2 [intro]: "(C::'a::plus set) \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C + E \<subseteq> D + F"
by (auto simp add: set_plus_def)
-lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
+lemma set_plus_mono3 [intro]: "a \<in> C \<Longrightarrow> a +o D \<subseteq> C + D"
by (auto simp add: elt_set_plus_def set_plus_def)
-lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
- a +o D <= D + C"
+lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) \<in> C \<Longrightarrow> a +o D \<subseteq> D + C"
by (auto simp add: elt_set_plus_def set_plus_def add_ac)
-lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
- apply (subgoal_tac "a +o B <= a +o D")
+lemma set_plus_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a +o B \<subseteq> C + D"
+ apply (subgoal_tac "a +o B \<subseteq> a +o D")
apply (erule order_trans)
apply (erule set_plus_mono3)
apply (erule set_plus_mono)
done
-lemma set_plus_mono_b: "C <= D ==> x : a +o C
- ==> x : a +o D"
+lemma set_plus_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a +o C \<Longrightarrow> x \<in> a +o D"
apply (frule set_plus_mono)
apply auto
done
-lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
- x : D + F"
+lemma set_plus_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C + E \<Longrightarrow> x \<in> D + F"
apply (frule set_plus_mono2)
prefer 2
apply force
apply assumption
done
-lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
+lemma set_plus_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> C + D"
apply (frule set_plus_mono3)
apply auto
done
-lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
- x : a +o D ==> x : D + C"
+lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> D + C"
apply (frule set_plus_mono4)
apply auto
done
@@ -182,28 +174,27 @@
lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
by (auto simp add: elt_set_plus_def)
-lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
+lemma set_zero_plus2: "(0::'a::comm_monoid_add) \<in> A \<Longrightarrow> B \<subseteq> A + B"
apply (auto simp add: set_plus_def)
apply (rule_tac x = 0 in bexI)
apply (rule_tac x = x in bexI)
apply (auto simp add: add_ac)
done
-lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
+lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C \<Longrightarrow> (a - b) \<in> C"
by (auto simp add: elt_set_plus_def add_ac)
-lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
+lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C \<Longrightarrow> a \<in> b +o C"
apply (auto simp add: elt_set_plus_def add_ac)
apply (subgoal_tac "a = (a + - b) + b")
apply (rule bexI, assumption)
apply (auto simp add: add_ac)
done
-lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
- by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
- assumption)
+lemma set_minus_plus: "(a::'a::ab_group_add) - b \<in> C \<longleftrightarrow> a \<in> b +o C"
+ by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus)
-lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
+lemma set_times_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a * b \<in> C * D"
by (auto simp add: set_times_def)
lemma set_times_elim:
@@ -211,11 +202,11 @@
obtains a b where "x = a * b" and "a \<in> A" and "b \<in> B"
using assms unfolding set_times_def by fast
-lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
+lemma set_times_intro2 [intro!]: "b \<in> C \<Longrightarrow> a * b \<in> a *o C"
by (auto simp add: elt_set_times_def)
-lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
- (b *o D) = (a * b) *o (C * D)"
+lemma set_times_rearrange:
+ "((a::'a::comm_monoid_mult) *o C) * (b *o D) = (a * b) *o (C * D)"
apply (auto simp add: elt_set_times_def set_times_def)
apply (rule_tac x = "ba * bb" in exI)
apply (auto simp add: mult_ac)
@@ -223,12 +214,12 @@
apply (auto simp add: mult_ac)
done
-lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
- (a * b) *o C"
+lemma set_times_rearrange2:
+ "(a::'a::semigroup_mult) *o (b *o C) = (a * b) *o C"
by (auto simp add: elt_set_times_def mult_assoc)
-lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
- a *o (B * C)"
+lemma set_times_rearrange3:
+ "((a::'a::semigroup_mult) *o B) * C = a *o (B * C)"
apply (auto simp add: elt_set_times_def set_times_def)
apply (blast intro: mult_ac)
apply (rule_tac x = "a * aa" in exI)
@@ -239,10 +230,9 @@
apply (auto simp add: mult_ac)
done
-theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
- a *o (C * D)"
- apply (auto simp add: elt_set_times_def set_times_def
- mult_ac)
+theorem set_times_rearrange4:
+ "C * ((a::'a::comm_monoid_mult) *o D) = a *o (C * D)"
+ apply (auto simp add: elt_set_times_def set_times_def mult_ac)
apply (rule_tac x = "aa * ba" in exI)
apply (auto simp add: mult_ac)
done
@@ -250,48 +240,43 @@
theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
set_times_rearrange3 set_times_rearrange4
-lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
+lemma set_times_mono [intro]: "C \<subseteq> D \<Longrightarrow> a *o C \<subseteq> a *o D"
by (auto simp add: elt_set_times_def)
-lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
- C * E <= D * F"
+lemma set_times_mono2 [intro]: "(C::'a::times set) \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C * E \<subseteq> D * F"
by (auto simp add: set_times_def)
-lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
+lemma set_times_mono3 [intro]: "a \<in> C \<Longrightarrow> a *o D \<subseteq> C * D"
by (auto simp add: elt_set_times_def set_times_def)
-lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
- a *o D <= D * C"
+lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C \<Longrightarrow> a *o D \<subseteq> D * C"
by (auto simp add: elt_set_times_def set_times_def mult_ac)
-lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
- apply (subgoal_tac "a *o B <= a *o D")
+lemma set_times_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a *o B \<subseteq> C * D"
+ apply (subgoal_tac "a *o B \<subseteq> a *o D")
apply (erule order_trans)
apply (erule set_times_mono3)
apply (erule set_times_mono)
done
-lemma set_times_mono_b: "C <= D ==> x : a *o C
- ==> x : a *o D"
+lemma set_times_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a *o C \<Longrightarrow> x \<in> a *o D"
apply (frule set_times_mono)
apply auto
done
-lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
- x : D * F"
+lemma set_times_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C * E \<Longrightarrow> x \<in> D * F"
apply (frule set_times_mono2)
prefer 2
apply force
apply assumption
done
-lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
+lemma set_times_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> C * D"
apply (frule set_times_mono3)
apply auto
done
-lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
- x : a *o D ==> x : D * C"
+lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> D * C"
apply (frule set_times_mono4)
apply auto
done
@@ -299,20 +284,19 @@
lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
by (auto simp add: elt_set_times_def)
-lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
- (a * b) +o (a *o C)"
+lemma set_times_plus_distrib:
+ "(a::'a::semiring) *o (b +o C) = (a * b) +o (a *o C)"
by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
-lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
- (a *o B) + (a *o C)"
+lemma set_times_plus_distrib2:
+ "(a::'a::semiring) *o (B + C) = (a *o B) + (a *o C)"
apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
apply blast
apply (rule_tac x = "b + bb" in exI)
apply (auto simp add: ring_distribs)
done
-lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
- a *o D + C * D"
+lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D \<subseteq> a *o D + C * D"
apply (auto simp add:
elt_set_plus_def elt_set_times_def set_times_def
set_plus_def ring_distribs)
@@ -323,12 +307,10 @@
set_times_plus_distrib
set_times_plus_distrib2
-lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
- - a : C"
+lemma set_neg_intro: "(a::'a::ring_1) \<in> (- 1) *o C \<Longrightarrow> - a \<in> C"
by (auto simp add: elt_set_times_def)
-lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
- - a : (- 1) *o C"
+lemma set_neg_intro2: "(a::'a::ring_1) \<in> C \<Longrightarrow> - a \<in> (- 1) *o C"
by (auto simp add: elt_set_times_def)
lemma set_plus_image: "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
@@ -337,53 +319,63 @@
lemma set_times_image: "S * T = (\<lambda>(x, y). x * y) ` (S \<times> T)"
unfolding set_times_def by (fastforce simp: image_iff)
-lemma finite_set_plus:
- assumes "finite s" and "finite t" shows "finite (s + t)"
- using assms unfolding set_plus_image by simp
+lemma finite_set_plus: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s + t)"
+ unfolding set_plus_image by simp
-lemma finite_set_times:
- assumes "finite s" and "finite t" shows "finite (s * t)"
- using assms unfolding set_times_image by simp
+lemma finite_set_times: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s * t)"
+ unfolding set_times_image by simp
lemma set_setsum_alt:
assumes fin: "finite I"
shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
(is "_ = ?setsum I")
-using fin proof induct
+ using fin
+proof induct
+ case empty
+ then show ?case by simp
+next
case (insert x F)
have "setsum S (insert x F) = S x + ?setsum F"
using insert.hyps by auto
- also have "...= {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
+ also have "\<dots> = {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
unfolding set_plus_def
proof safe
- fix y s assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
+ fix y s
+ assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
then show "\<exists>s'. y + setsum s F = s' x + setsum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)"
using insert.hyps
by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def)
qed auto
finally show ?case
using insert.hyps by auto
-qed auto
+qed
lemma setsum_set_cond_linear:
- fixes f :: "('a::comm_monoid_add) set \<Rightarrow> ('b::comm_monoid_add) set"
+ fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
assumes [intro!]: "\<And>A B. P A \<Longrightarrow> P B \<Longrightarrow> P (A + B)" "P {0}"
and f: "\<And>A B. P A \<Longrightarrow> P B \<Longrightarrow> f (A + B) = f A + f B" "f {0} = {0}"
assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
shows "f (setsum S I) = setsum (f \<circ> S) I"
-proof cases
- assume "finite I" from this all show ?thesis
+proof (cases "finite I")
+ case True
+ from this all show ?thesis
proof induct
+ case empty
+ then show ?case by (auto intro!: f)
+ next
case (insert x F)
from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum S F)"
by induct auto
with insert show ?case
by (simp, subst f) auto
- qed (auto intro!: f)
-qed (auto intro!: f)
+ qed
+next
+ case False
+ then show ?thesis by (auto intro!: f)
+qed
lemma setsum_set_linear:
- fixes f :: "('a::comm_monoid_add) set => ('b::comm_monoid_add) set"
+ fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
assumes "\<And>A B. f(A) + f(B) = f(A + B)" "f {0} = {0}"
shows "f (setsum S I) = setsum (f \<circ> S) I"
using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
@@ -391,11 +383,11 @@
lemma set_times_Un_distrib:
"A * (B \<union> C) = A * B \<union> A * C"
"(A \<union> B) * C = A * C \<union> B * C"
-by (auto simp: set_times_def)
+ by (auto simp: set_times_def)
lemma set_times_UNION_distrib:
- "A * UNION I M = UNION I (%i. A * M i)"
- "UNION I M * A = UNION I (%i. M i * A)"
-by (auto simp: set_times_def)
+ "A * UNION I M = (\<Union>i\<in>I. A * M i)"
+ "UNION I M * A = (\<Union>i\<in>I. M i * A)"
+ by (auto simp: set_times_def)
end
--- a/src/HOL/SPARK/Tools/spark_commands.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Wed May 07 14:51:51 2014 +0200
@@ -123,8 +123,7 @@
val _ =
Outer_Syntax.command @{command_spec "spark_vc"}
"enter into proof mode for a specific verification condition"
- (Parse.name >> (fn name =>
- (Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name))));
+ (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
val _ =
Outer_Syntax.improper_command @{command_spec "spark_status"}
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed May 07 14:51:51 2014 +0200
@@ -666,7 +666,6 @@
val _ =
Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively"
(Scan.repeat1 Parse.term >> (fn ts =>
- Toplevel.print o
Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts)));
end;
--- a/src/HOL/Tools/choice_specification.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/Tools/choice_specification.ML Wed May 07 14:51:51 2014 +0200
@@ -201,7 +201,6 @@
Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
(@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
- >> (fn (cos, alt_props) => Toplevel.print o
- (Toplevel.theory_to_proof (process_spec cos alt_props))))
+ >> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))
end
--- a/src/Pure/Isar/calculation.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/calculation.ML Wed May 07 14:51:51 2014 +0200
@@ -118,9 +118,9 @@
val ctxt' = Proof.context_of state';
val _ =
if int then
- Pretty.writeln
- (Proof_Context.pretty_fact ctxt'
- (Proof_Context.full_name ctxt' (Binding.name calculationN), calc))
+ Proof_Context.pretty_fact ctxt'
+ (Proof_Context.full_name ctxt' (Binding.name calculationN), calc)
+ |> Pretty.string_of |> Output.urgent_message
else ();
in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
--- a/src/Pure/Isar/isar_syn.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed May 07 14:51:51 2014 +0200
@@ -404,14 +404,12 @@
val _ =
Outer_Syntax.command @{command_spec "include"}
"include declarations from bundle in proof body"
- (Scan.repeat1 (Parse.position Parse.xname)
- >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
+ (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
val _ =
Outer_Syntax.command @{command_spec "including"}
"include declarations from bundle in goal refinement"
- (Scan.repeat1 (Parse.position Parse.xname)
- >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
+ (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
val _ =
Outer_Syntax.improper_command @{command_spec "print_bundles"}
@@ -425,7 +423,7 @@
val _ =
Outer_Syntax.command @{command_spec "context"} "begin local theory context"
((Parse.position Parse.xname >> (fn name =>
- Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
+ Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
>> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
--| Parse.begin);
@@ -443,7 +441,7 @@
(Parse.binding --
Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
- (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+ Toplevel.begin_local_theory begin
(Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
fun interpretation_args mandatory =
@@ -456,24 +454,20 @@
"prove sublocale relation between a locale and a locale expression"
((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
interpretation_args false >> (fn (loc, (expr, equations)) =>
- Toplevel.print o
Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
|| interpretation_args false >> (fn (expr, equations) =>
- Toplevel.print o
Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
val _ =
Outer_Syntax.command @{command_spec "interpretation"}
"prove interpretation of locale expression in local theory"
(interpretation_args true >> (fn (expr, equations) =>
- Toplevel.print o
Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
val _ =
Outer_Syntax.command @{command_spec "interpret"}
"prove interpretation of locale expression in proof context"
(interpretation_args true >> (fn (expr, equations) =>
- Toplevel.print o
Toplevel.proof' (Expression.interpret_cmd expr equations)));
@@ -488,7 +482,7 @@
Outer_Syntax.command @{command_spec "class"} "define type class"
(Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
- (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+ Toplevel.begin_local_theory begin
(Class_Declaration.class_cmd I name supclasses elems #> snd)));
val _ =
@@ -498,17 +492,14 @@
val _ =
Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
(Parse.multi_arity --| Parse.begin
- >> (fn arities => Toplevel.print o
- Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
+ >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
val _ =
Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
((Parse.class --
((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
- Parse.multi_arity >> Class.instance_arity_cmd)
- >> (Toplevel.print oo Toplevel.theory_to_proof) ||
- Scan.succeed
- (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
+ Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
+ Scan.succeed (Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
(* arbitrary overloading *)
@@ -518,8 +509,7 @@
(Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
>> Parse.triple1) --| Parse.begin
- >> (fn operations => Toplevel.print o
- Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
+ >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
(* code generation *)
@@ -559,20 +549,20 @@
val _ =
Outer_Syntax.command @{command_spec "have"} "state local goal"
- (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
+ (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
val _ =
Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
- (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
+ (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
val _ =
Outer_Syntax.command @{command_spec "show"}
"state local goal, solving current obligation"
- (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
+ (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
val _ =
Outer_Syntax.command @{command_spec "thus"} "old-style alias of \"then show\""
- (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
+ (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
(* facts *)
@@ -581,42 +571,42 @@
val _ =
Outer_Syntax.command @{command_spec "then"} "forward chaining"
- (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
+ (Scan.succeed (Toplevel.proof Proof.chain));
val _ =
Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
+ (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
val _ =
Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
+ (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
val _ =
Outer_Syntax.command @{command_spec "note"} "define facts"
- (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
+ (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
val _ =
Outer_Syntax.command @{command_spec "using"} "augment goal facts"
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
+ (facts >> (Toplevel.proof o Proof.using_cmd));
val _ =
Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
+ (facts >> (Toplevel.proof o Proof.unfolding_cmd));
(* proof context *)
val _ =
Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
- (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
+ (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
val _ =
Outer_Syntax.command @{command_spec "assume"} "assume propositions"
- (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
+ (Parse_Spec.statement >> (Toplevel.proof o Proof.assume_cmd));
val _ =
Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
- (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
+ (Parse_Spec.statement >> (Toplevel.proof o Proof.presume_cmd));
val _ =
Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
@@ -624,26 +614,26 @@
(Parse_Spec.opt_thm_name ":" --
((Parse.binding -- Parse.opt_mixfix) --
((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
- >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
+ >> (Toplevel.proof o Proof.def_cmd));
val _ =
Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
(Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
- >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
+ >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
val _ =
Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
- (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
+ (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
val _ =
Outer_Syntax.command @{command_spec "let"} "bind text variables"
(Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
- >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
+ >> (Toplevel.proof o Proof.let_bind_cmd));
val _ =
Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
(opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
- >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
+ >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
val _ =
Outer_Syntax.command @{command_spec "case"} "invoke local context"
@@ -651,22 +641,22 @@
Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
--| @{keyword ")"}) ||
Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
- Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
+ Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
(* proof structure *)
val _ =
Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
- (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
+ (Scan.succeed (Toplevel.proof Proof.begin_block));
val _ =
Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
- (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
+ (Scan.succeed (Toplevel.proof Proof.end_block));
val _ =
Outer_Syntax.command @{command_spec "next"} "enter next proof block"
- (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
+ (Scan.succeed (Toplevel.proof Proof.next_block));
(* end proof *)
@@ -675,61 +665,58 @@
Outer_Syntax.command @{command_spec "qed"} "conclude proof"
(Scan.option Method.parse >> (fn m =>
(Option.map Method.report m;
- Toplevel.print o Isar_Cmd.qed m)));
+ Isar_Cmd.qed m)));
val _ =
Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
(Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
(Method.report m1;
Option.map Method.report m2;
- Toplevel.print o Isar_Cmd.terminal_proof (m1, m2))));
+ Isar_Cmd.terminal_proof (m1, m2))));
val _ =
Outer_Syntax.command @{command_spec ".."} "default proof"
- (Scan.succeed (Toplevel.print o Isar_Cmd.default_proof));
+ (Scan.succeed Isar_Cmd.default_proof);
val _ =
Outer_Syntax.command @{command_spec "."} "immediate proof"
- (Scan.succeed (Toplevel.print o Isar_Cmd.immediate_proof));
+ (Scan.succeed Isar_Cmd.immediate_proof);
val _ =
Outer_Syntax.command @{command_spec "done"} "done proof"
- (Scan.succeed (Toplevel.print o Isar_Cmd.done_proof));
+ (Scan.succeed Isar_Cmd.done_proof);
val _ =
Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
- (Scan.succeed (Toplevel.print o Isar_Cmd.skip_proof));
+ (Scan.succeed Isar_Cmd.skip_proof);
val _ =
Outer_Syntax.command @{command_spec "oops"} "forget proof"
- (Scan.succeed (Toplevel.print o Toplevel.forget_proof));
+ (Scan.succeed Toplevel.forget_proof);
(* proof steps *)
val _ =
Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
- (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
+ (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
val _ =
Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
- (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
+ (Parse.nat >> (Toplevel.proof o Proof.prefer));
val _ =
Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
- (Method.parse >> (fn m =>
- (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_results m))));
+ (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
val _ =
Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
- (Method.parse >> (fn m =>
- (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_end_results m))));
+ (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
val _ =
Outer_Syntax.command @{command_spec "proof"} "backward proof step"
(Scan.option Method.parse >> (fn m =>
(Option.map Method.report m;
- Toplevel.print o
Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
Toplevel.skip_proof (fn i => i + 1))));
@@ -741,8 +728,8 @@
val _ =
Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
- (Scan.succeed (Toplevel.print o
- Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
+ (Scan.succeed
+ (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
Toplevel.skip_proof (fn h => (report_back (); h))));
@@ -792,8 +779,9 @@
Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
- (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_state_context)));
+ Outer_Syntax.improper_command @{command_spec "print_context"}
+ "print context of local theory target"
+ (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
val _ =
Outer_Syntax.improper_command @{command_spec "print_theory"}
--- a/src/Pure/Isar/keyword.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/keyword.ML Wed May 07 14:51:51 2014 +0200
@@ -67,6 +67,7 @@
val is_proof_goal: string -> bool
val is_qed: string -> bool
val is_qed_global: string -> bool
+ val is_printed: string -> bool
end;
structure Keyword: KEYWORD =
@@ -263,5 +264,7 @@
val is_qed = command_category [qed, qed_script, qed_block];
val is_qed_global = command_category [qed_global];
+val is_printed = is_theory_goal orf is_proof;
+
end;
--- a/src/Pure/Isar/obtain.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/obtain.ML Wed May 07 14:51:51 2014 +0200
@@ -300,7 +300,7 @@
val goal = Var (("guess", 0), propT);
fun print_result ctxt' (k, [(s, [_, th])]) =
- Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
+ Proof_Display.print_results int ctxt' (k, [(s, [th])]);
val before_qed =
Method.primitive_text (fn ctxt =>
Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
--- a/src/Pure/Isar/outer_syntax.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed May 07 14:51:51 2014 +0200
@@ -203,14 +203,13 @@
(* local_theory commands *)
-fun local_theory_command do_print trans command_spec comment parse =
- command command_spec comment (Parse.opt_target -- parse
- >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
+fun local_theory_command trans command_spec comment parse =
+ command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));
-val local_theory' = local_theory_command false Toplevel.local_theory';
-val local_theory = local_theory_command false Toplevel.local_theory;
-val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
-val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
+val local_theory' = local_theory_command Toplevel.local_theory';
+val local_theory = local_theory_command Toplevel.local_theory;
+val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
+val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
(* inspect syntax *)
--- a/src/Pure/Isar/proof.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/proof.ML Wed May 07 14:51:51 2014 +0200
@@ -365,8 +365,7 @@
else if mode = Backward then Proof_Context.pretty_ctxt ctxt
else [];
in
- [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
- (if verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")),
+ [Pretty.str ("proof (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1)),
Pretty.str ""] @
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
(if verbose orelse mode = Forward then
@@ -1042,7 +1041,7 @@
local
fun gen_have prep_att prepp before_qed after_qed stmt int =
- local_goal (Proof_Display.print_results Markup.state int)
+ local_goal (Proof_Display.print_results int)
prep_att prepp "have" before_qed after_qed stmt;
fun gen_show prep_att prepp before_qed after_qed stmt int state =
@@ -1056,7 +1055,7 @@
fun print_results ctxt res =
if ! testing then ()
- else Proof_Display.print_results Markup.state int ctxt res;
+ else Proof_Display.print_results int ctxt res;
fun print_rule ctxt th =
if ! testing then rule := SOME th
else if int then
--- a/src/Pure/Isar/proof_display.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML Wed May 07 14:51:51 2014 +0200
@@ -22,8 +22,7 @@
val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
val method_error: string -> Position.T ->
{context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
- val print_results: Markup.T -> bool -> Proof.context ->
- ((string * string) * (string * thm list) list) -> unit
+ val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
end
@@ -141,13 +140,13 @@
in
-fun print_results markup do_print ctxt ((kind, name), facts) =
+fun print_results do_print ctxt ((kind, name), facts) =
if not do_print orelse kind = "" then ()
else if name = "" then
- (Pretty.writeln o Pretty.mark markup)
+ (Pretty.writeln o Pretty.mark Markup.state)
(Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
else
- (Pretty.writeln o Pretty.mark markup)
+ (Pretty.writeln o Pretty.mark Markup.state)
(case facts of
[fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
Proof_Context.pretty_fact ctxt fact])
@@ -176,7 +175,7 @@
fun print_consts do_print ctxt pred cs =
if not do_print orelse null cs then ()
- else Pretty.writeln (pretty_consts ctxt pred cs);
+ else Pretty.writeln (Pretty.mark Markup.state (pretty_consts ctxt pred cs));
end;
--- a/src/Pure/Isar/specification.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/specification.ML Wed May 07 14:51:51 2014 +0200
@@ -301,7 +301,7 @@
|> Attrib.partial_evaluation ctxt'
|> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
- val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res);
+ val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
in (res, lthy') end;
in
@@ -400,12 +400,12 @@
(map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
val lthy'' =
if Attrib.is_empty_binding (name, atts) then
- (Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res); lthy')
+ (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
else
let
val ([(res_name, _)], lthy'') =
Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
- val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, res_name), res);
+ val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
in lthy'' end;
in after_qed results' lthy'' end;
in
--- a/src/Pure/Isar/toplevel.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed May 07 14:51:51 2014 +0200
@@ -22,7 +22,7 @@
val proof_of: state -> Proof.state
val proof_position_of: state -> int
val end_theory: Position.T -> state -> theory
- val pretty_state_context: state -> Pretty.T list
+ val pretty_context: state -> Pretty.T list
val pretty_state: state -> Pretty.T list
val print_state: state -> unit
val pretty_abstract: state -> Pretty.T
@@ -32,14 +32,11 @@
val profiling: int Unsynchronized.ref
type transition
val empty: transition
- val print_of: transition -> bool
val name_of: transition -> string
val pos_of: transition -> Position.T
val name: string -> transition -> transition
val position: Position.T -> transition -> transition
val interactive: bool -> transition -> transition
- val set_print: bool -> transition -> transition
- val print: transition -> transition
val init_theory: (unit -> theory) -> transition -> transition
val is_init: transition -> bool
val modify_init: (unit -> theory) -> transition -> transition
@@ -198,14 +195,18 @@
(* print state *)
-val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
-
-fun pretty_state_context state =
+fun pretty_context state =
(case try node_of state of
NONE => []
- | SOME (Theory (gthy, _)) => pretty_context gthy
- | SOME (Proof (_, (_, gthy))) => pretty_context gthy
- | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy);
+ | SOME node =>
+ let
+ val gthy =
+ (case node of
+ Theory (gthy, _) => gthy
+ | Proof (_, (_, gthy)) => gthy
+ | Skipped_Proof (_, (gthy, _)) => gthy);
+ val lthy = Context.cases (Named_Target.theory_init) I gthy;
+ in Local_Theory.pretty lthy end);
fun pretty_state state =
(case try node_of state of
@@ -312,23 +313,21 @@
{name: string, (*command name*)
pos: Position.T, (*source position*)
int_only: bool, (*interactive-only*) (* TTY / Proof General legacy*)
- print: bool, (*print result state*)
timing: Time.time option, (*prescient timing information*)
trans: trans list}; (*primitive transitions (union)*)
-fun make_transition (name, pos, int_only, print, timing, trans) =
- Transition {name = name, pos = pos, int_only = int_only, print = print,
+fun make_transition (name, pos, int_only, timing, trans) =
+ Transition {name = name, pos = pos, int_only = int_only,
timing = timing, trans = trans};
-fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) =
- make_transition (f (name, pos, int_only, print, timing, trans));
+fun map_transition f (Transition {name, pos, int_only, timing, trans}) =
+ make_transition (f (name, pos, int_only, timing, trans));
-val empty = make_transition ("", Position.none, false, false, NONE, []);
+val empty = make_transition ("", Position.none, false, NONE, []);
(* diagnostics *)
-fun print_of (Transition {print, ...}) = print;
fun name_of (Transition {name, ...}) = name;
fun pos_of (Transition {pos, ...}) = pos;
@@ -341,25 +340,20 @@
(* modify transitions *)
-fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) =>
- (name, pos, int_only, print, timing, trans));
+fun name name = map_transition (fn (_, pos, int_only, timing, trans) =>
+ (name, pos, int_only, timing, trans));
-fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) =>
- (name, pos, int_only, print, timing, trans));
-
-fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) =>
- (name, pos, int_only, print, timing, trans));
+fun position pos = map_transition (fn (name, _, int_only, timing, trans) =>
+ (name, pos, int_only, timing, trans));
-fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) =>
- (name, pos, int_only, print, timing, tr :: trans));
+fun interactive int_only = map_transition (fn (name, pos, _, timing, trans) =>
+ (name, pos, int_only, timing, trans));
-val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) =>
- (name, pos, int_only, print, timing, []));
+fun add_trans tr = map_transition (fn (name, pos, int_only, timing, trans) =>
+ (name, pos, int_only, timing, tr :: trans));
-fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) =>
- (name, pos, int_only, print, timing, trans));
-
-val print = set_print true;
+val reset_trans = map_transition (fn (name, pos, int_only, timing, _) =>
+ (name, pos, int_only, timing, []));
(* basic transitions *)
@@ -415,6 +409,10 @@
let
val lthy = f thy;
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
+ val _ =
+ if begin then
+ Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
+ else ();
in Theory (gthy, SOME lthy) end
| _ => raise UNDEF));
@@ -579,19 +577,22 @@
(* apply transitions *)
fun get_timing (Transition {timing, ...}) = timing;
-fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
- (name, pos, int_only, print, timing, trans));
+fun put_timing timing = map_transition (fn (name, pos, int_only, _, trans) =>
+ (name, pos, int_only, timing, trans));
local
-fun app int (tr as Transition {trans, print, ...}) =
+fun app int (tr as Transition {name, trans, ...}) =
setmp_thread_position tr (fn state =>
let
val timing_start = Timing.start ();
val (result, opt_err) =
state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
- val _ = if int andalso not (! quiet) andalso print then print_state result else ();
+
+ val _ =
+ if int andalso not (! quiet) andalso Keyword.is_printed name
+ then print_state result else ();
val timing_result = Timing.result timing_start;
val timing_props =
@@ -739,7 +740,7 @@
(fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
val st'' = st'
- |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
+ |> command (head_tr |> reset_trans |> forked_proof);
val end_result = Result (end_tr, st'');
val result =
Result_List [head_result, Result.get (presentation_context_of st''), end_result];
--- a/src/Pure/PIDE/command.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/PIDE/command.ML Wed May 07 14:51:51 2014 +0200
@@ -226,12 +226,10 @@
else
let
val malformed' = Toplevel.is_malformed tr;
- val is_init = Toplevel.is_init tr;
- val is_proof = Keyword.is_proof (Toplevel.name_of tr);
val _ = Multithreading.interrupted ();
val _ = status tr Markup.running;
- val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+ val (errs1, result) = run true tr st;
val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
val errs = errs1 @ errs2;
val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
@@ -376,15 +374,10 @@
val _ =
print_function "print_state"
(fn {command_name, ...} =>
- SOME {delay = NONE, pri = 1, persistent = false, strict = true,
- print_fn = fn tr => fn st' =>
- let
- val is_init = Keyword.is_theory_begin command_name;
- val is_proof = Keyword.is_proof command_name;
- val do_print =
- not is_init andalso
- (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
- in if do_print then Toplevel.print_state st' else () end});
+ if Keyword.is_printed command_name then
+ SOME {delay = NONE, pri = 1, persistent = false, strict = true,
+ print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
+ else NONE);
(* combined execution *)
--- a/src/Pure/System/isabelle_process.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed May 07 14:51:51 2014 +0200
@@ -200,7 +200,7 @@
val channel = rendezvous ();
val msg_channel = init_channels channel;
val _ = Session.init_protocol_handlers ();
- val _ = loop channel;
+ val _ = (loop |> Unsynchronized.setmp Toplevel.quiet true) channel;
in Message_Channel.shutdown msg_channel end);
fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
--- a/src/Pure/Tools/build.scala Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/build.scala Wed May 07 14:51:51 2014 +0200
@@ -288,7 +288,8 @@
if (is_session_dir(dir)) dir
else error("Bad session root directory: " + dir.toString)
- def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
+ def find_sessions(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil)
+ : Session_Tree =
{
def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
find_root(select, dir) ::: find_roots(select, dir)
@@ -320,13 +321,13 @@
else Nil
}
- val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
-
- more_dirs foreach { case (_, dir) => check_session_dir(dir) }
+ val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
+ dirs.foreach(check_session_dir(_))
+ select_dirs.foreach(check_session_dir(_))
Session_Tree(
for {
- (select, dir) <- default_dirs ::: more_dirs
+ (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
info <- find_dir(select, dir)
} yield info)
}
@@ -511,8 +512,7 @@
dirs: List[Path],
sessions: List[String]): Deps =
{
- val (_, tree) =
- find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, sessions)
+ val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
dependencies(Ignore_Progress, inlined_files, false, false, tree)
}
@@ -722,7 +722,8 @@
all_sessions: Boolean = false,
build_heap: Boolean = false,
clean_build: Boolean = false,
- more_dirs: List[(Boolean, Path)] = Nil,
+ dirs: List[Path] = Nil,
+ select_dirs: List[Path] = Nil,
session_groups: List[String] = Nil,
max_jobs: Int = 1,
list_files: Boolean = false,
@@ -733,7 +734,7 @@
{
/* session tree and dependencies */
- val full_tree = find_sessions(options, more_dirs)
+ val full_tree = find_sessions(options, dirs, select_dirs)
val (selected, selected_tree) =
full_tree.selection(requirements, all_sessions, session_groups, sessions)
@@ -972,7 +973,8 @@
all_sessions: Boolean = false,
build_heap: Boolean = false,
clean_build: Boolean = false,
- more_dirs: List[(Boolean, Path)] = Nil,
+ dirs: List[Path] = Nil,
+ select_dirs: List[Path] = Nil,
session_groups: List[String] = Nil,
max_jobs: Int = 1,
list_files: Boolean = false,
@@ -983,8 +985,8 @@
{
val results =
build_results(options, progress, requirements, all_sessions,
- build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
- system_mode, verbose, sessions)
+ build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
+ list_files, no_build, system_mode, verbose, sessions)
val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
if (rc != 0 && (verbose || !no_build)) {
@@ -1012,16 +1014,13 @@
Properties.Value.Boolean(no_build) ::
Properties.Value.Boolean(system_mode) ::
Properties.Value.Boolean(verbose) ::
- Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
+ Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
val options = (Options.init() /: build_options)(_ + _)
- val more_dirs =
- select_dirs.map(d => (true, Path.explode(d))) :::
- include_dirs.map(d => (false, Path.explode(d)))
val progress = new Console_Progress(verbose)
progress.interrupt_handler {
- build(options, progress, requirements, all_sessions,
- build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
- system_mode, verbose, sessions)
+ build(options, progress, requirements, all_sessions, build_heap, clean_build,
+ dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
+ max_jobs, list_files, no_build, system_mode, verbose, sessions)
}
case _ => error("Bad arguments:\n" + cat_lines(args))
}
--- a/src/Pure/Tools/build_doc.scala Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/build_doc.scala Wed May 07 14:51:51 2014 +0200
@@ -24,7 +24,7 @@
{
val selection =
for {
- (name, info) <- Build.find_sessions(options, Nil).topological_order
+ (name, info) <- Build.find_sessions(options).topological_order
if info.groups.contains("doc")
doc = info.options.string("document_variants")
if all_docs || docs.contains(doc)
--- a/src/Pure/Tools/find_consts.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML Wed May 07 14:51:51 2014 +0200
@@ -113,7 +113,9 @@
|> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
|> map (apsnd fst o snd);
in
- Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
+ Pretty.block
+ (Pretty.keyword1 "find_consts" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
+ Pretty.fbreaks (map pretty_criterion raw_criteria)) ::
Pretty.str "" ::
Pretty.str
(if null matches
--- a/src/Pure/Tools/find_theorems.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed May 07 14:51:51 2014 +0200
@@ -483,7 +483,9 @@
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
in
- Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
+ Pretty.block
+ (Pretty.keyword1 "find_theorems" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
+ Pretty.fbreaks (map (pretty_criterion ctxt) criteria)) ::
Pretty.str "" ::
(if null theorems then [Pretty.str "nothing found"]
else
--- a/src/Pure/Tools/keywords.scala Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/keywords.scala Wed May 07 14:51:51 2014 +0200
@@ -150,7 +150,7 @@
def update_keywords(options: Options)
{
- val tree = Build.find_sessions(options, Nil)
+ val tree = Build.find_sessions(options)
def chapter(ch: String): List[String] =
for ((name, info) <- tree.topological_order if info.chapter == ch) yield name
--- a/src/Pure/Tools/main.scala Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/main.scala Wed May 07 14:51:51 2014 +0200
@@ -41,13 +41,13 @@
else {
val options = Options.init()
val system_mode = mode == "" || mode == "system"
- val more_dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).map((false, _))
+ val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
val session = Isabelle_System.default_logic(
Isabelle_System.getenv("JEDIT_LOGIC"),
options.string("jedit_logic"))
if (Build.build(options = options, build_heap = true, no_build = true,
- more_dirs = more_dirs, sessions = List(session)) == 0)
+ dirs = dirs, sessions = List(session)) == 0)
system_dialog.return_code(0)
else {
system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")")
@@ -56,9 +56,8 @@
val (out, rc) =
try {
("",
- Build.build(options = options, progress = system_dialog,
- build_heap = true, more_dirs = more_dirs,
- system_mode = system_mode, sessions = List(session)))
+ Build.build(options = options, progress = system_dialog, build_heap = true,
+ dirs = dirs, system_mode = system_mode, sessions = List(session)))
}
catch {
case exn: Throwable =>
--- a/src/Pure/Tools/print_operation.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML Wed May 07 14:51:51 2014 +0200
@@ -61,8 +61,8 @@
(* common print operations *)
val _ =
- register "context" "main context"
- (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state_context);
+ register "context" "context of local theory target"
+ (Pretty.string_of o Pretty.chunks o Toplevel.pretty_context);
val _ =
register "cases" "cases of proof context"
--- a/src/Pure/pure_syn.ML Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/pure_syn.ML Wed May 07 14:51:51 2014 +0200
@@ -11,9 +11,8 @@
Outer_Syntax.command
(("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
(Thy_Header.args >> (fn header =>
- Toplevel.print o
- Toplevel.init_theory
- (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
+ Toplevel.init_theory
+ (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
val _ =
Outer_Syntax.command
--- a/src/Tools/jEdit/src/isabelle_logic.scala Wed May 07 12:25:35 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed May 07 14:51:51 2014 +0200
@@ -71,8 +71,7 @@
def session_list(): List[String] =
{
- val dirs = session_dirs().map((false, _))
- val session_tree = Build.find_sessions(PIDE.options.value, dirs)
+ val session_tree = Build.find_sessions(PIDE.options.value, dirs = session_dirs())
val (main_sessions, other_sessions) =
session_tree.topological_order.partition(p => p._2.groups.contains("main"))
main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
--- a/src/Tools/jEdit/src/jEdit.props Wed May 07 12:25:35 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Wed May 07 14:51:51 2014 +0200
@@ -243,6 +243,7 @@
recent-buffer.shortcut2=C+CIRCUMFLEX
restore.remote=false
restore=false
+search.subdirs.toggle=true
select-block.shortcut2=C+8
sidekick-tree.dock-position=right
sidekick.auto-complete-popup-get-focus=true