equal
deleted
inserted
replaced
1441 lemma finfun_to_list_update_code [code]: |
1441 lemma finfun_to_list_update_code [code]: |
1442 "finfun_to_list (finfun_update_code f a b) = |
1442 "finfun_to_list (finfun_update_code f a b) = |
1443 (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))" |
1443 (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))" |
1444 by(simp add: finfun_to_list_update) |
1444 by(simp add: finfun_to_list_update) |
1445 |
1445 |
|
1446 text {* Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again *} |
|
1447 |
|
1448 no_type_notation |
|
1449 finfun ("(_ =>f /_)" [22, 21] 21) |
|
1450 |
|
1451 no_type_notation (xsymbols) |
|
1452 finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21) |
|
1453 |
|
1454 no_notation |
|
1455 finfun_const ("K$/ _" [0] 1) and |
|
1456 finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and |
|
1457 finfun_apply (infixl "$" 999) and |
|
1458 finfun_comp (infixr "o$" 55) and |
|
1459 finfun_comp2 (infixr "$o" 55) and |
|
1460 finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000) |
|
1461 |
|
1462 no_notation (xsymbols) |
|
1463 finfun_comp (infixr "\<circ>$" 55) and |
|
1464 finfun_comp2 (infixr "$\<circ>" 55) |
|
1465 |
1446 end |
1466 end |