Pearl-jv/Paper.thy
changeset 2747 a5da7b6aff8f
parent 2746 6aa98a113e6c
child 2754 2a3a37f29f4f
equal deleted inserted replaced
2746:6aa98a113e6c 2747:a5da7b6aff8f
     1 (*<*)
     1 (*<*)
     2 theory Paper
     2 theory Paper
     3 imports "../Nominal/Nominal2_Base" 
     3 imports "../Nominal/Nominal2_Base" 
     4         "../Nominal/Atoms" 
     4         "../Nominal/Atoms" 
     5         "../Nominal/Nominal2_Abs"
     5         "../Nominal/Nominal2_Abs"
     6         "LaTeXsugar"
     6         "~~/src/HOL/Library/LaTeXsugar"
     7 begin
     7 begin
     8 
     8 
     9 abbreviation
     9 abbreviation
    10  UNIV_atom ("\<allatoms>")
    10  UNIV_atom ("\<allatoms>")
    11 where
    11 where