Pearl/Paper.thy
changeset 1774 c34347ec7ab3
parent 1772 48c2eb84d5ce
child 1776 0c958e385691
equal deleted inserted replaced
1773:c0eac04ae3b4 1774:c34347ec7ab3
     1 (*<*)
     1 (*<*)
     2 theory Paper
     2 theory Paper
     3 imports "../Nominal/Nominal2_Base" 
     3 imports "../Nominal-General/Nominal2_Base" 
     4         "../Nominal/Nominal2_Atoms" 
     4         "../Nominal-General/Nominal2_Atoms" 
     5         "../Nominal/Nominal2_Eqvt" 
     5         "../Nominal-General/Nominal2_Eqvt" 
     6         "../Nominal/Atoms" 
     6         "../Nominal-General/Atoms" 
     7         "LaTeXsugar"
     7         "LaTeXsugar"
     8 begin
     8 begin
     9 
     9 
    10 notation (latex output)
    10 notation (latex output)
    11   sort_of ("sort _" [1000] 100) and
    11   sort_of ("sort _" [1000] 100) and