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
Sun, 20 Oct 2019 20:38:22 +0200
changeset 70915 bd4d37edfee4
parent 63167 0909deb8059b
permissions -rw-r--r--
clarified expand_proof/expand_name: allow more detailed control via thm_header; export_standard_proofs: authentic theorem names in "print" format;
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
 







63167






0909deb8059b
isabelle update_cartouches -c -t;



wenzelm


parents: 
58889

diff
changeset




     6


section \<open>Main HOL Light importer\<close>








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