# HG changeset patch
# User nipkow
# Date 1546774321 -3600
# Node ID 86e8e7347ac00fcfb7e01f4b0fa779824697bc69
# Parent  caa7e406056d7627d5ec2d04a0b66ad081420321
typed definitions

diff -r caa7e406056d -r 86e8e7347ac0 src/HOL/Analysis/Abstract_Topology.thy
--- 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")
diff -r caa7e406056d -r 86e8e7347ac0 src/HOL/Analysis/Inner_Product.thy
--- 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
diff -r caa7e406056d -r 86e8e7347ac0 src/HOL/Analysis/L2_Norm.thy
--- 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"
diff -r caa7e406056d -r 86e8e7347ac0 src/HOL/Analysis/Linear_Algebra.thy
--- 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)"