--- a/src/HOL/Analysis/Abstract_Topology.thy Sat Jan 05 20:12:02 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Sun Jan 06 12:32:01 2019 +0100
@@ -13,7 +13,8 @@
subsection \<open>General notion of a topology as a value\<close>
-definition%important "istopology L \<longleftrightarrow>
+definition%important istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
+"istopology L \<longleftrightarrow>
L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
@@ -113,7 +114,8 @@
subsubsection \<open>Closed sets\<close>
-definition%important "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
+definition%important closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
+"closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
by (metis closedin_def)
@@ -230,7 +232,8 @@
subsection \<open>Subspace topology\<close>
-definition%important "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
+definition%important subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" where
+"subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
(is "istopology ?L")
--- a/src/HOL/Analysis/Inner_Product.thy Sat Jan 05 20:12:02 2019 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy Sun Jan 06 12:32:01 2019 +0100
@@ -2,7 +2,7 @@
Author: Brian Huffman
*)
-section \<open>Inner Product Spaces and the Gradient Derivative\<close>
+section \<open>Inner Product Spaces and Gradient Derivative\<close>
theory Inner_Product
imports Complex_Main
--- a/src/HOL/Analysis/L2_Norm.thy Sat Jan 05 20:12:02 2019 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy Sun Jan 06 12:32:01 2019 +0100
@@ -8,7 +8,8 @@
imports Complex_Main
begin
-definition %important "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
+definition%important L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where
+"L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
lemma L2_set_cong:
"\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
--- a/src/HOL/Analysis/Linear_Algebra.thy Sat Jan 05 20:12:02 2019 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Sun Jan 06 12:32:01 2019 +0100
@@ -183,7 +183,9 @@
subsection \<open>Bilinear functions\<close>
-definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
+definition%important
+bilinear :: "('a::real_vector \<Rightarrow> 'b::real_vector \<Rightarrow> 'c::real_vector) \<Rightarrow> bool" where
+"bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
by (simp add: bilinear_def linear_iff)
@@ -239,7 +241,8 @@
subsection \<open>Adjoints\<close>
-definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
+definition%important adjoint :: "(('a::real_inner) \<Rightarrow> ('b::real_inner)) \<Rightarrow> 'b \<Rightarrow> 'a" where
+"adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
lemma adjoint_unique:
assumes "\<forall>x y. inner (f x) y = inner x (g y)"