The following is a LALR(1) grammar with precedence declarations for a subset of Isabelle/HOL formulas.

/* Terminals (tokens returned by the scanner). */
terminal EQUALS, AND, ASSIGN, UNION, ALL, EX, NOT, DOT, LPAREN, RPAREN;
terminal LCURLYBRACKET, RCURLYBRACKET, COMMA;
terminal String    ID;

/* Non-terminals */
non terminal            boundform;
non terminal            boundform_list;
non terminal            formula;
non terminal            factor;
non terminal            set_expr;
non terminal            factor_list;
non terminal            factor_comma_list;
non terminal            variable;
non terminal            varList;

/* Precedences */
precedence left         AND;
precedence left         EQUALS;
precedence left		UNION;
precedence left         NOT;

/* The grammar */
start with boundform;

variable         ::= ID;

boundform        ::= ALL varList | EX varList | formula;

varList          ::= variable DOT boundform
                  |  variable varList;

formula          ::= formula AND formula
                  |  formula UNION formula 
                  |  formula EQUALS formula
                  |  NOT formula
                  |  factor_list;

factor           ::= variable
                  |  set_expr
                  |  LPAREN boundform_list RPAREN;

boundform_list ::= boundform
	         | boundform_list COMMA boundform;

set_expr         ::= LCURLYBRACKET RCURLYBRACKET
                  |  LCURLYBRACKET factor_comma_list RCURLYBRACKET
		  |  LCURLYBRACKET factor_comma_list DOT boundform RCURLYBRACKET;

factor_comma_list ::= factor
		   |  factor_comma_list COMMA factor;

factor_list      ::= factor
	           | factor_list factor
	           | factor_list LPAREN factor ASSIGN factor_list RPAREN;