2079   (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term}

  2079   (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term}

  2080   are of any use/efficient)

  2080   are of any use/efficient)

  2081 *}

  2081 *}

  2082 

  2082 

  2083 

  2083 

  2084 section {* Structured Proofs (TBD) *}

  2086 section {* Structured Proofs (TBD) *}

  2085 

  2087 

  2086 text {* TBD *}

  2088 text {* TBD *}

  2087 

  2089 

  2088 lemma True

  2090 lemma True