src/HOL/TLA/Inc/ROOT.ML
changeset 3823 071c87125cea
child 9000 c20d58286a51
equal deleted inserted replaced
3822:a17f9b8dca93 3823:071c87125cea
       
     1 
       
     2 use_thy "Inc";