4 

     4 

     5 (*<*)

     5 (*<*)

     6 setup{*

     6 setup{*

     7 open_file_with_prelude 

     7 open_file_with_prelude 

     8   "Essential_Code.thy"

     8   "Essential_Code.thy"

    10 *}

    10 *}

    11 (*>*)

    11 (*>*)

    12 

    12 

    13 

    13 

    14 chapter {* Isabelle Essentials *}

    14 chapter {* Isabelle Essentials *}

  1642 

  1642 

  1643   @{ML_response_fake [display, gray]

  1643   @{ML_response_fake [display, gray]

  1644   "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"

  1644   "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"

  1645   "True = False"}

  1645   "True = False"}

  1646 

  1646 

  1650   Theorems also contain auxiliary data, such as the name of the theorem, its

  1647   Theorems also contain auxiliary data, such as the name of the theorem, its

  1651   kind, the names for cases and so on. This data is stored in a string-string

  1648   kind, the names for cases and so on. This data is stored in a string-string

  1652   list and can be retrieved with the function @{ML_ind get_tags in

  1649   list and can be retrieved with the function @{ML_ind get_tags in

  1653   Thm}. Assume you prove the following lemma.

  1650   Thm}. Assume you prove the following lemma.

  1654 *}

  1651 *}