# HG changeset patch
# User Andreas Lochbihler
# Date 1338386706 -7200
# Node ID d60f6b41bf2de934a2cd1e306a1b6bb1244030c1
# Parent  daab96c3e2a9d72a692efadaa86022c077c02772
remove pretty syntax for FinFuns at the end and provide separate syntax theory

diff -r daab96c3e2a9 -r d60f6b41bf2d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed May 30 10:04:05 2012 +0200
+++ b/src/HOL/IsaMakefile	Wed May 30 16:05:06 2012 +0200
@@ -455,7 +455,7 @@
   Library/DAList.thy Library/Dlist.thy					\
   Library/Eval_Witness.thy						\
   Library/Extended_Real.thy Library/Extended_Nat.thy			\
-  Library/FinFun.thy Library/Float.thy					\
+  Library/FinFun.thy Library/FinFun_Syntax.thy Library/Float.thy	\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
   Library/FrechetDeriv.thy Library/FuncSet.thy				\
   Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy	\
diff -r daab96c3e2a9 -r d60f6b41bf2d src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Wed May 30 10:04:05 2012 +0200
+++ b/src/HOL/Library/FinFun.thy	Wed May 30 16:05:06 2012 +0200
@@ -1443,4 +1443,24 @@
   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
 by(simp add: finfun_to_list_update)
 
+text {* Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again *}
+
+no_type_notation
+  finfun ("(_ =>f /_)" [22, 21] 21)
+
+no_type_notation (xsymbols)
+  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
+
+no_notation
+  finfun_const ("K$/ _" [0] 1) and
+  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
+  finfun_apply (infixl "$" 999) and
+  finfun_comp (infixr "o$" 55) and
+  finfun_comp2 (infixr "$o" 55) and
+  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
+
+no_notation (xsymbols) 
+  finfun_comp (infixr "\<circ>$" 55) and
+  finfun_comp2 (infixr "$\<circ>" 55)
+
 end
diff -r daab96c3e2a9 -r d60f6b41bf2d src/HOL/Library/FinFun_Syntax.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/FinFun_Syntax.thy	Wed May 30 16:05:06 2012 +0200
@@ -0,0 +1,25 @@
+(* Author: Andreas Lochbihler, KIT *)
+
+header {* Pretty syntax for almost everywhere constant functions *}
+
+theory FinFun_Syntax imports FinFun begin
+
+type_notation
+  finfun ("(_ =>f /_)" [22, 21] 21)
+
+type_notation (xsymbols)
+  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
+
+notation
+  finfun_const ("K$/ _" [0] 1) and
+  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
+  finfun_apply (infixl "$" 999) and
+  finfun_comp (infixr "o$" 55) and
+  finfun_comp2 (infixr "$o" 55) and
+  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
+
+notation (xsymbols) 
+  finfun_comp (infixr "\<circ>$" 55) and
+  finfun_comp2 (infixr "$\<circ>" 55)
+
+end
\ No newline at end of file
diff -r daab96c3e2a9 -r d60f6b41bf2d src/HOL/ex/FinFunPred.thy
--- a/src/HOL/ex/FinFunPred.thy	Wed May 30 10:04:05 2012 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Wed May 30 16:05:06 2012 +0200
@@ -4,7 +4,7 @@
   Predicates modelled as FinFuns
 *}
 
-theory FinFunPred imports "~~/src/HOL/Library/FinFun" begin
+theory FinFunPred imports "~~/src/HOL/Library/FinFun_Syntax" begin
 
 text {* Instantiate FinFun predicates just like predicates *}
 
diff -r daab96c3e2a9 -r d60f6b41bf2d src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed May 30 10:04:05 2012 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed May 30 16:05:06 2012 +0200
@@ -12,7 +12,7 @@
   "Hebrew",
   "Chinese",
   "Serbian",
-  "~~/src/HOL/Library/FinFun"
+  "~~/src/HOL/Library/FinFun_Syntax"
 ];
 
 use_thys [