# HG changeset patch # User wenzelm # Date 1727123617 -7200 # Node ID b5bdcdbf5ec1cebc8a034d3396a4837b7291f6ec # Parent 8e72f55295fd9caf41b0b698dc35ddf77e5e8419 proper 'no_syntax' (amending 8e72f55295fd); diff -r 8e72f55295fd -r b5bdcdbf5ec1 src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Mon Sep 23 21:09:23 2024 +0200 +++ b/src/HOL/Nominal/Examples/Fsub.thy Mon Sep 23 22:33:37 2024 +0200 @@ -17,7 +17,7 @@ section \Types for Names, Nominal Datatype Declaration for Types and Terms\ no_syntax - "_Map" :: "maplets => 'a \ 'b" (\(1[_])\) + "_Map" :: "maplets => 'a \ 'b" (\(\indent=1 notation=\mixfix maplets\\[_])\) text \The main point of this solution is to use names everywhere (be they bound, binding or free). In System \FSUB{} there are two kinds of names corresponding to diff -r 8e72f55295fd -r b5bdcdbf5ec1 src/HOL/Nominal/Examples/Pattern.thy --- a/src/HOL/Nominal/Examples/Pattern.thy Mon Sep 23 21:09:23 2024 +0200 +++ b/src/HOL/Nominal/Examples/Pattern.thy Mon Sep 23 22:33:37 2024 +0200 @@ -5,7 +5,7 @@ begin no_syntax - "_Map" :: "maplets => 'a \ 'b" (\(1[_])\) + "_Map" :: "maplets => 'a \ 'b" (\(\indent=1 notation=\mixfix maplets\\[_])\) atom_decl name