# HG changeset patch # User wenzelm # Date 1465593184 -7200 # Node ID a59801b7f125d0ef9dec25747d26de671fa80272 # Parent 7c509ddf29a517a3d9306f80572e01b8fe4be2e0 bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax; diff -r 7c509ddf29a5 -r a59801b7f125 NEWS --- a/NEWS Fri Jun 10 22:47:25 2016 +0200 +++ b/NEWS Fri Jun 10 23:13:04 2016 +0200 @@ -148,6 +148,11 @@ * Probability/SPMF formalises discrete subprobability distributions. +* Library/FinFun.thy: bundles "finfun_syntax" and "no_finfun_syntax" +allow to control optional syntax in local contexts; this supersedes +former Library/FinFun_Syntax.thy. INCOMPATIBILITY, e.g. use "unbundle +finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax". + * Library/Set_Permutations.thy (executably) defines the set of permutations of a set, i.e. the set of all lists that contain every element of the carrier set exactly once. diff -r 7c509ddf29a5 -r a59801b7f125 src/HOL/Library/FinFun.thy --- a/src/HOL/Library/FinFun.thy Fri Jun 10 22:47:25 2016 +0200 +++ b/src/HOL/Library/FinFun.thy Fri Jun 10 23:13:04 2016 +0200 @@ -1534,14 +1534,38 @@ instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun) end -text \Deactivate syntax again. Import theory \FinFun_Syntax\ to reactivate it again\ + +subsubsection \Bundles for concrete syntax\ + +bundle finfun_syntax +begin + +type_notation finfun ("(_ \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 "\$" 55) and + finfun_comp2 (infixr "$\" 55) and + finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000) + +notation (ASCII) + finfun_comp (infixr "o$" 55) and + finfun_comp2 (infixr "$o" 55) + +end + + +bundle no_finfun_syntax +begin no_type_notation finfun ("(_ \f /_)" [22, 21] 21) no_notation finfun_const ("K$/ _" [0] 1) and - finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and + finfun_update ("_'(_ $:= _')" [1000, 0, 0] 1000) and finfun_apply (infixl "$" 999) and finfun_comp (infixr "\$" 55) and finfun_comp2 (infixr "$\" 55) and @@ -1552,3 +1576,7 @@ finfun_comp2 (infixr "$o" 55) end + +unbundle no_finfun_syntax + +end diff -r 7c509ddf29a5 -r a59801b7f125 src/HOL/Library/FinFun_Syntax.thy --- a/src/HOL/Library/FinFun_Syntax.thy Fri Jun 10 22:47:25 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* Author: Andreas Lochbihler, KIT *) - -section \Pretty syntax for almost everywhere constant functions\ - -theory FinFun_Syntax -imports FinFun -begin - -type_notation - finfun ("(_ \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 "\$" 55) and - finfun_comp2 (infixr "$\" 55) and - finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000) - -notation (ASCII) - finfun_comp (infixr "o$" 55) and - finfun_comp2 (infixr "$o" 55) - -end diff -r 7c509ddf29a5 -r a59801b7f125 src/HOL/ROOT --- a/src/HOL/ROOT Fri Jun 10 22:47:25 2016 +0200 +++ b/src/HOL/ROOT Fri Jun 10 23:13:04 2016 +0200 @@ -545,7 +545,6 @@ Hebrew Chinese Serbian - "~~/src/HOL/Library/FinFun_Syntax" "~~/src/HOL/Library/Refute" "~~/src/HOL/Library/Transitive_Closure_Table" Cartouche_Examples diff -r 7c509ddf29a5 -r a59801b7f125 src/HOL/ex/FinFunPred.thy --- a/src/HOL/ex/FinFunPred.thy Fri Jun 10 22:47:25 2016 +0200 +++ b/src/HOL/ex/FinFunPred.thy Fri Jun 10 23:13:04 2016 +0200 @@ -1,10 +1,12 @@ (* Author: Andreas Lochbihler *) -section \ - Predicates modelled as FinFuns -\ +section \Predicates modelled as FinFuns\ -theory FinFunPred imports "~~/src/HOL/Library/FinFun_Syntax" begin +theory FinFunPred +imports "~~/src/HOL/Library/FinFun" +begin + +unbundle finfun_syntax text \Instantiate FinFun predicates just like predicates\