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 haftmann
Fri, 15 Feb 2013 08:31:31 +0100
changeset 51143 0a2371e7ced3
parent 47266 bf9796e44584
child 58889 5b7a9633cfa8
permissions -rw-r--r--
two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
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
 












880e587eee9f
Modernized HOL-Import for HOL Light



Cezary Kaliszyk <cezarykaliszyk@gmail.com>


parents: 

diff
changeset




     6


header {* Main HOL Light importer *}













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