795 

   795 

   796 

   796 

   797 *}

   797 *}

   798 

   798 

   799 section {* Parsing Specifications\label{sec:parsingspecs} *}

   799 section {* Parsing Specifications\label{sec:parsingspecs} *}

   800 

   801 

   801 text {*

   802 text {*

   802   There are a number of special purpose parsers that help with parsing

   803   There are a number of special purpose parsers that help with parsing

   803   specifications of function definitions, inductive predicates and so on. In

   804   specifications of function definitions, inductive predicates and so on. In

   804   Chapter~\ref{chp:package}, for example, we will need to parse specifications

   805   Chapter~\ref{chp:package}, for example, we will need to parse specifications

  1510 lemma "True"

  1511 lemma "True"

  1511 apply(test)

  1512 apply(test)

  1512 oops

  1513 oops

  1513 

  1514 

  1514 method_setup joker = {* 

  1515 method_setup joker = {* 

  1516 

  1517 

  1517 lemma "False"

  1518 lemma "False"

  1518 apply(joker)

  1519 apply(joker)

  1519 oops

  1520 oops

  1520 

  1521