| 
25
 | 
     1  | 
session "Hoare_gen" = "HOL" +
  | 
| 
 | 
     2  | 
  options [document = pdf]
  | 
| 
 | 
     3  | 
  theories [document = false]
  | 
| 
 | 
     4  | 
     Hoare_gen
  | 
| 
 | 
     5  | 
  | 
| 
 | 
     6  | 
session "Hoare_tm_basis" = "Hoare_gen" +
  | 
| 
 | 
     7  | 
  options [document = pdf]
  | 
| 
 | 
     8  | 
  theories [document = false, document_output = "output_tm", document_variants = "hoare_tm"]
  | 
| 
 | 
     9  | 
     Hoare_tm_basis
  | 
| 
 | 
    10  | 
  | 
| 
 | 
    11  | 
session "Hoare_tm" = "Hoare_tm_basis" +
  | 
| 
 | 
    12  | 
  options [document = pdf]
  | 
| 
 | 
    13  | 
  theories [document = false, document_output = "output_tm", document_variants = "hoare_tm"]
  | 
| 
 | 
    14  | 
     Hoare_tm
  | 
| 
 | 
    15  | 
  | 
| 
 | 
    16  | 
session "Hoare_abc" = "Hoare_tm" +
  | 
| 
 | 
    17  | 
  options [document = pdf]
  | 
| 
 | 
    18  | 
  theories [document = false, document_output = "./output_abc"]
  | 
| 
 | 
    19  | 
     Hoare_abc
  | 
| 
 | 
    20  | 
  |