diff --git a/content/http..mathhub.info/MitM/Models/poisson/$Displacement$Law.omdoc b/content/http..mathhub.info/MitM/Models/poisson/$Displacement$Law.omdoc
index 1ff8b452d220290fb8b079ace9e014071f0b1a58..321919a705660585d67bc400a99c648b0b75b15b 100644
--- a/content/http..mathhub.info/MitM/Models/poisson/$Displacement$Law.omdoc
+++ b/content/http..mathhub.info/MitM/Models/poisson/$Displacement$Law.omdoc
@@ -1,6 +1,6 @@
 <omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="DisplacementLaw" base="http://mathhub.info/MitM/Models/poisson" meta="http://mathhub.info/MitM/Models?Base"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1171.29.0:1469.38.1"/></metadata><import from="http://mathhub.info/MitM/Models/densities?ElectrostaticPotential"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1209.30.1:1250.30.42"/></metadata></import><import from="http://mathhub.info/MitM/Models/poisson?PoissonParameters"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1253.31.1:1280.31.28"/></metadata></import><import from="http://mathhub.info/MitM/Models/poisson?Displacement"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1283.32.1:1305.32.23"/></metadata></import><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1310.34.1:1386.34.77"/></metadata>Expression for electric displacement denoted by <unparsed>None</unparsed> = <unparsed>None</unparsed> d/dx <unparsed>None</unparsed></opaque><constant name="electric_displacement">
        <metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1390.36.1:1467.37.30"/></metadata>
-       <type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[Ω → displacement_dim]]></om:text></om:OMSF></om:OMOBJ></type>
+       <type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[Ω ⟶ displacement_dim]]></om:text></om:OMSF></om:OMOBJ></type>
        <definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[[x] -ε_s ⋅ (ψ ' x)]]></om:text></om:OMSF></om:OMOBJ></definition>
        <notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="D"> <scope languages="" priority="0"/> </notation></notations>
      </constant></theory></omdoc>
\ No newline at end of file
diff --git a/content/http..mathhub.info/MitM/Models/thermistor/$Spatial$Reference$Electrical$Field.omdoc b/content/http..mathhub.info/MitM/Models/thermistor/$Spatial$Reference$Electrical$Field.omdoc
index 78cd8532cbf05803b1700d15acaac4b6854bba9a..5ad6858730657c0f80ded642a6af081892433b3a 100644
--- a/content/http..mathhub.info/MitM/Models/thermistor/$Spatial$Reference$Electrical$Field.omdoc
+++ b/content/http..mathhub.info/MitM/Models/thermistor/$Spatial$Reference$Electrical$Field.omdoc
@@ -1,6 +1,6 @@
 <omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="SpatialReferenceElectricalField" base="http://mathhub.info/MitM/Models/thermistor" meta="http://mathhub.info/MitM/Models?Base"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/thermistor/quantities.mmt#2155.71.0:2342.75.-1"/></metadata><import from="http://mathhub.info/MitM/Models/thermistor?DeviceGeometry"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/thermistor/quantities.mmt#2210.72.2:2234.72.26"/></metadata></import><import from="http://mathhub.info/MitM/Models/thermistor?ElectricalFieldStrength"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/thermistor/quantities.mmt#2238.73.2:2271.73.35"/></metadata></import><constant name="referebceelectricfield">
        <metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/thermistor/quantities.mmt#2275.74.2:2341.74.68"/></metadata>
-       <type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[Ω → (electricfieldstrength_dim)]]></om:text></om:OMSF></om:OMOBJ></type>
+       <type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[Ω ⟶ (electricfieldstrength_dim)]]></om:text></om:OMSF></om:OMOBJ></type>
        
        <notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="Eref"> <scope languages="" priority="0"/> </notation></notations>
      </constant></theory></omdoc>
\ No newline at end of file
diff --git a/source/mmt/Quantities.mmt b/source/mmt/Quantities.mmt
index 5691860a1c9c5496cc96af2ede0eb3a840534994..62112664321cd1c1a26af963084d28ed81fe9e10 100644
--- a/source/mmt/Quantities.mmt
+++ b/source/mmt/Quantities.mmt
@@ -31,12 +31,12 @@ theory RecombinationRate : qe:?SIUnits =
 	include Models/device?DeviceGeometry ❙
   // meta modeltype physical_quantity ❙
 	recombinationrate_dim : dimension ❘ = DimNone /' (Volume *' Time) ❙
-	recombinationrate : Ω → QE recombinationrate_dim ❘ # R ❘ role Quantity ❙
+	recombinationrate : Ω ⟶ QE recombinationrate_dim ❘ # R ❘ role Quantity ❙
 ❚
 	
 theory RecombinationCoefficient : qe:?SIUnits =
 	include ?Density ❙
-	recombination_coefficient : QE density_dim → QE density_dim → QE (Volume /' Time) ❘ # r ❘ role Quantity ❙
+	recombination_coefficient : QE density_dim ⟶ QE density_dim ⟶ QE (Volume /' Time) ❘ # r ❘ role Quantity ❙
 ❚                                          
 	
 theory Energy : qe:?SIUnits =
@@ -46,7 +46,7 @@ theory Energy : qe:?SIUnits =
 theory SpatialDensity : qe:?SIUnits =
 	include Models/device?DeviceGeometry ❙
 	include ?Density ❙
-	spatialdensity : Ω → QE density_dim ❘ # n ❘ role Quantity ❙
+	spatialdensity : Ω ⟶ QE density_dim ❘ # n ❘ role Quantity ❙
 ❚
 	
 theory SpatialPotential : qe:?SIUnits =
@@ -54,17 +54,17 @@ theory SpatialPotential : qe:?SIUnits =
   /T Spatial variation of the potential,
 
 usually denoted by $φ$. ❙
-	potential : Ω → (QE ElectricPotential) ❘ # φ ❘ role Quantity ❙	
+	potential : Ω ⟶ (QE ElectricPotential) ❘ # φ ❘ role Quantity ❙	
 ❚
 	
 theory SpatialChargeDensity : qe:?SIUnits =
 	include Models/device?DeviceGeometry ❙
 	include ?Density ❙
-	charge : Ω → QE (ElectricCharge *' density_dim) ❘ # Q ❘ role Quantity ❙
+	charge : Ω ⟶ QE (ElectricCharge *' density_dim) ❘ # Q ❘ role Quantity ❙
 ❚
 
 theory SpatialCurrentDensity : qe:?SIUnits =
    include Models/device?DeviceGeometry ❙
    include ?CurrentDensity ❙
-	spatialcurrentdensity : Ω → QE currentdensity_dim ❘ # j ❘ role Quantity ❙
+	spatialcurrentdensity : Ω ⟶ QE currentdensity_dim ❘ # j ❘ role Quantity ❙
 ❚
diff --git a/source/mmt/constants.mmt b/source/mmt/constants.mmt
index dc989a9985cc4fc0bcfe05d89bb42e80390d8dc9..92cd845c20e66804d879b2512e608f83e31b79bf 100644
--- a/source/mmt/constants.mmt
+++ b/source/mmt/constants.mmt
@@ -19,17 +19,17 @@ theory Base : mitm:/smglom/arithmetics?realarith =
 	include ?PhysicalConstants ❙                                 
 	include http://mathhub.info/MitM/smglom/calculus?derivative ❙
 	// TODO anständige ableitung (Einheiten!!) ❙                             
-	unit_pred : {D : dimension, P : ℝ → bool} type ❘
+	unit_pred : {D : dimension, P : ℝ ⟶ bool} type ❘
 		= [D,P] ⟨ QE D | [x] ⊦ P (scalar x) ⟩ ❘ # dpred 1 2 ❙
-	inof : {D : dimension, u : unit D, P : ℝ → bool, r : pred P}dpred D P ❘ # 4 inof 2 ❙ // TODO ❙
-	scalarp : {D : dimension, P : ℝ → bool} dpred D P → pred P ❘ # scalarp 3 ❙
+	inof : {D : dimension, u : unit D, P : ℝ ⟶ bool, r : pred P}dpred D P ❘ # 4 inof 2 ❙ // TODO ❙
+	scalarp : {D : dimension, P : ℝ ⟶ bool} dpred D P ⟶ pred P ❘ # scalarp 3 ❙
 	
 	rule rules?QuantityRule ❙
 	rule rules?LawRule ❙
 	rule rules?ModelRule ❙
 	
 	// TODO ❙
-	// unit_derivative : {P : ℝ → bool, Da : dimension, Db : dimension, u : unit Da, f : (dpred Da P) → QE Db, p : ⊦ diff [x : pred P] scalar (f (x inof u))} dpred Da P → QE Db ❘
+	// unit_derivative : {P : ℝ ⟶ bool, Da : dimension, Db : dimension, u : unit Da, f : (dpred Da P) ⟶ QE Db, p : ⊦ diff [x : pred P] scalar (f (x inof u))} dpred Da P ⟶ QE Db ❘
 		= [P,Da,Db,u,f,p] ([y] ([x : pred P] (scalar (f (x inof u)))' (scalarp y)) of (unitof y) ) ❙
 	
 	// Ω = kompakte, einfach zusammenhängende teilmenge des ℝ^n  für n ‍∈ 4 ❙
diff --git a/source/mmt/device.mmt b/source/mmt/device.mmt
index dfb5f888b75dadde7170d4359c69bb6adf5e5dcc..4e3b9b0e9af6d8bfbcc7c80ed89ed9f3f87e5c5a 100644
--- a/source/mmt/device.mmt
+++ b/source/mmt/device.mmt
@@ -9,8 +9,8 @@ theory Device = ❚
 /T   Parameter ❚
 theory DeviceGeometry : top:?Base =
 	include ?Device ❙
-	// domain_prop : ℝ3 → bool ❙
-	domain_prop : ℝ → bool ❙
+	// domain_prop : ℝ3 ⟶ bool ❙
+	domain_prop : ℝ ⟶ bool ❙
 	/T The one-dimensional spatial domain of the device (denoted by $Ω$). ❙
 	// domain : type ❘ = pred3 domain_prop ❘ # Ω ❙
 	domain : type ❘ = pred domain_prop ❘ # Ω ❙
@@ -19,7 +19,7 @@ theory DeviceGeometry : top:?Base =
 //   theory OneDimDeviceGeometry : top:?Base =
 	bottom : ℝ ❙
 	top : ℝ ❙
-	Interval_pred : ℝ → bool ❘ = [r] bottom ≤ r ∧ r ≤ top ❙
+	Interval_pred : ℝ ⟶ bool ❘ = [r] bottom ≤ r ∧ r ≤ top ❙
 	Omega_Interval : type ❘ = pred Interval_pred ❘ # I ❙ 
 	
 	structure Geometry : ?DeviceGeometry =
@@ -28,7 +28,7 @@ theory DeviceGeometry : top:?Base =
 //   ❚
 
 //   theory TwoDimDeviceGeometry : top:?Base =
-	Plane_pred : ℝ2 → bool ❙
+	Plane_pred : ℝ2 ⟶ bool ❙
 	Omega_Plane : type ❘ = pred2 Plane_pred ❘ # G ❙
 	
 	structure Geometry : ?DeviceGeometry =
@@ -42,7 +42,7 @@ theory DopingProfile : top:?Base =
 	include ?DeviceGeometry ❙
 	include top:?Density ❙
   /T The doping profile, denoted by $C$. ❙
-	doping_profile : Ω →  QE density_dim ❘ # C ❙
+	doping_profile : Ω ⟶  QE density_dim ❘ # C ❙
 ❚
 
 	
@@ -52,7 +52,7 @@ theory DopingProfile : top:?Base =
 theory DeviceOperationState : top:?Base =
 	include ?DeviceGeometry ❙
 	/T The global temperature of the device denoted by $T$. ❙
-	// temperature : Ω → ℝ ❘ # T ❙
+	// temperature : Ω ⟶ ℝ ❘ # T ❙
 	temperature : QE Temperature ❘ # T ❙
 	/T The applied voltage at the bottom contact denoted by $U_1$. ❙
 	voltage_bottom : QE ElectricPotential ❘ # U_1 ❙
diff --git a/source/mmt/poisson.mmt b/source/mmt/poisson.mmt
index 7f77a038445b6bc3488f36238761d74ae185d84a..59429f2a1dab914565a74caa8f45be9feb7e0777 100644
--- a/source/mmt/poisson.mmt
+++ b/source/mmt/poisson.mmt
@@ -34,7 +34,7 @@ theory ChargeLaw : top:?Base =
 	
 	/T Expression for electric displacement denoted by $D$ = $- ε_s$ d/dx $ψ$  ❙
 	
-	electric_displacement : Ω → displacement_dim ❘
+	electric_displacement : Ω ⟶ displacement_dim ❘
 		= [x] -ε_s ⋅ (ψ ' x) ❘ # D ❙
 ❚
 		
diff --git a/source/thermistor/quantities.mmt b/source/thermistor/quantities.mmt
index 9010f75ad71e633dd013d2ebe8c796d2f6f1c0dd..cf6e4dc0462740922d1e7bd0ee991ac02b41ebf2 100644
--- a/source/thermistor/quantities.mmt
+++ b/source/thermistor/quantities.mmt
@@ -10,8 +10,8 @@ theory Device = ❚
 /T   Parameter ❚
 theory DeviceGeometry : top:?Base =
 	include ?Device ❙
-	// domain_prop : ℝ3 → bool ❙
-	domain_prop : ℝ → bool ❙
+	// domain_prop : ℝ3 ⟶ bool ❙
+	domain_prop : ℝ ⟶ bool ❙
 	/T The one-dimensional spatial domain of the device (denoted by $Ω$). ❙
 	domain : type ❘ = pred domain_prop ❘ # Ω ❙
 ❚
@@ -20,7 +20,7 @@ theory SpatialPotential : top:?Base =
   include ?DeviceGeometry ❙
   /T Spatial variation of the potential,
 	   usually denoted by $φ$. ❙
-	potential : Ω → (QE ElectricPotential) ❘ # φ❙	
+	potential : Ω ⟶ (QE ElectricPotential) ❘ # φ❙	
 ❚
 
 theory ElectricFieldStrength : qe:?QEBase =
@@ -34,7 +34,7 @@ theory SpatialElectricField : top:?Base =
   include ?ElectricFieldStrength ❙
   /T Spatial variation of the electric field strength,
 	   usually denoted by $E$. ❙
-	electricfield : Ω → (electricfieldstrength_dim) ❘ # E❙	
+	electricfield : Ω ⟶ (electricfieldstrength_dim) ❘ # E❙	
 ❚
 
 theory CurrentDensity : qe:?QEBase =
@@ -47,7 +47,7 @@ theory CurrentDensity : qe:?QEBase =
 theory SpatialCurrentDensity : top:?Base =
   include ?DeviceGeometry ❙
   include ?CurrentDensity ❙
-	currentdensity : Ω → (currentdensity_dim) ❘ # j 1 ❙
+	currentdensity : Ω ⟶ (currentdensity_dim) ❘ # j 1 ❙
 ❚
 
 theory ElectricalConductivity : qe:?QEBase =
@@ -60,34 +60,34 @@ theory ElectricalConductivity : qe:?QEBase =
 theory SpatialElectricalConductivity : top:?Base =
   include ?DeviceGeometry ❙
   include ?ElectricalConductivity ❙
-	spatialelectricalconductivity : Ω → (electricalconductitvity_dim) ❘ # σ 1 ❙
+	spatialelectricalconductivity : Ω ⟶ (electricalconductitvity_dim) ❘ # σ 1 ❙
 ❚
 
 theory SpatialReferenceConductivity : top:?Base =
   include ?DeviceGeometry ❙
   include ?ElectricalConductivity ❙
-	spatialreferenceconductivity : Ω → (electricalconductitvity_dim) ❘ # σ_0 1 ❙
+	spatialreferenceconductivity : Ω ⟶ (electricalconductitvity_dim) ❘ # σ_0 1 ❙
 ❚
 	
 theory SpatialReferenceElectricalField : top:?Base =
   include ?DeviceGeometry ❙
   include ?ElectricalFieldStrength ❙
-  referebceelectricfield : Ω → (electricfieldstrength_dim) ❘ # Eref❙	
+  referebceelectricfield : Ω ⟶ (electricfieldstrength_dim) ❘ # Eref❙	
 ❚
 	
 theory SpatialFieldEnhancement : top:?Base =
    include ?DeviceGeometry ❙
-   spatialfieldenhancement :  Ω → ℝ ❘ # G❙	
+   spatialfieldenhancement :  Ω ⟶ ℝ ❘ # G❙	
 ❚
 
 theory SpatialLaplacep : top:?Base =
    include ?DeviceGeometry ❙
-   spatiallaplacep :  Ω → ℝ ❘ # p❙	
+   spatiallaplacep :  Ω ⟶ ℝ ❘ # p❙	
 ❚
       
 theory SpatialArrheniusFaktor : top:?Base =
    include ?DeviceGeometry ❙
-   spatialarrheniusfaktor :  Ω → ℝ ❘ # F❙	   
+   spatialarrheniusfaktor :  Ω ⟶ ℝ ❘ # F❙	   
 ❚
    
 theory Heat : qe:?QEBase =
@@ -99,13 +99,13 @@ theory Heat : qe:?QEBase =
 theory SpatialHeatSource : top:?Base =
   include ?DeviceGeometry ❙
   include ?Heat ❙
-	spatialheatsource : Ω → (heat_dim) ❘ # Q 1 ❙
+	spatialheatsource : Ω ⟶ (heat_dim) ❘ # Q 1 ❙
 ❚
 
 theory SpatialJouleHeat : top:?Base =
   include ?DeviceGeometry ❙
   include ?Heat ❙
-	spatialheatsource : Ω → (heat_dim) ❘ # Q_Joule 1 ❙
+	spatialheatsource : Ω ⟶ (heat_dim) ❘ # Q_Joule 1 ❙
 ❚
 
 theory ThermalConductivity : qe:?QEBase =
@@ -118,7 +118,7 @@ theory ThermalConductivity : qe:?QEBase =
 theory SpatialThermalConductivity : top:?Base =
   include ?DeviceGeometry ❙
   include ?ThermalConductivity ❙
-	spatialthermalconductivity : Ω → (thermalconductitvity_dim) ❘ # λ 1 ❙
+	spatialthermalconductivity : Ω ⟶ (thermalconductitvity_dim) ❘ # λ 1 ❙
 ❚
 
 theory ThermalHeatFlux : qe:?QEBase =
@@ -130,14 +130,14 @@ theory ThermalHeatFlux : qe:?QEBase =
 theory SpatialHeatFluxDensity : top:?Base =
   include ?DeviceGeometry ❙
   include ?ThermalHeatFlux ❙
-	heatfluxdensity : Ω → (thermalheatflux_dim) ❘ # q 1 ❙
+	heatfluxdensity : Ω ⟶ (thermalheatflux_dim) ❘ # q 1 ❙
 ❚
 	  
 theory SpatialTemperature : top:?Base =
   include ?DeviceGeometry ❙
   /T Spatial variation of the potential,
 	   usually denoted by $φ$. ❙
-	potential : Ω → (QE SItemperature) ❘ # T❙	
+	potential : Ω ⟶ (QE SItemperature) ❘ # T❙	
 ❚
 
 theory ReferenceTemperature : top:?Base =