Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL_Light_Import.thy
author wenzelm
Thu, 30 Apr 2015 15:58:15 +0200
changeset 60159 879918f4ee0f
parent 58889 5b7a9633cfa8
child 63167 0909deb8059b
permissions -rw-r--r--
tuned -- avoid odd rebinding of "ctxt" and "context";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47258
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset 
     1
 
(*  Title:      HOL/Import/HOL_Light_Import.thy
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset 
     2
 
    Author:     Cezary Kaliszyk, University of Innsbruck
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset 
     3
 
    Author:     Alexander Krauss, QAware GmbH
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset 
     4
 
*)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset 
     5
 







58889






5b7a9633cfa8
modernized header uniformly as section;



wenzelm


parents: 
47266

diff
changeset




     6


section {* Main HOL Light importer *}








47258






880e587eee9f
Modernized HOL-Import for HOL Light



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 

diff
changeset




     7














880e587eee9f
Modernized HOL-Import for HOL Light



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 

diff
changeset




     8


theory HOL_Light_Import













880e587eee9f
Modernized HOL-Import for HOL Light



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 

diff
changeset




     9


imports HOL_Light_Maps













880e587eee9f
Modernized HOL-Import for HOL Light



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 

diff
changeset




    10


begin













880e587eee9f
Modernized HOL-Import for HOL Light



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 

diff
changeset




    11









47266






bf9796e44584
clarified terminology; added reference to bundle component



krauss


parents: 
47258

diff
changeset




    12


import_file "$HOL_LIGHT_BUNDLE"








47258






880e587eee9f
Modernized HOL-Import for HOL Light



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 

diff
changeset




    13














880e587eee9f
Modernized HOL-Import for HOL Light



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 

diff
changeset




    14


end













880e587eee9f
Modernized HOL-Import for HOL Light



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 

diff
changeset




    15
















isabelle