src/HOL/Codegenerator_Test/Generate_Target_Nat.thy
changeset 58889 5b7a9633cfa8
parent 51161 6ed12ae3b3e1
child 63167 0909deb8059b
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     1 
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     3 
     4 header {* Pervasive test of code generator *}
     4 section {* Pervasive test of code generator *}
     5 
     5 
     6 theory Generate_Target_Nat
     6 theory Generate_Target_Nat
     7 imports
     7 imports
     8   Candidates
     8   Candidates
     9   "~~/src/HOL/Library/AList_Mapping"
     9   "~~/src/HOL/Library/AList_Mapping"