src/HOL/Record.thy
changeset 38539 3be65f879bcd
parent 38530 048338a9b389
child 41229 d797baa3d57c
     1.1 --- a/src/HOL/Record.thy	Wed Aug 18 15:01:57 2010 +0200
     1.2 +++ b/src/HOL/Record.thy	Wed Aug 18 16:59:35 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  theory Record
     1.6  imports Plain Quickcheck
     1.7 -uses ("Tools/quickcheck_record.ML") ("Tools/record.ML")
     1.8 +uses ("Tools/record.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Introduction *}
    1.12 @@ -452,7 +452,6 @@
    1.13  
    1.14  subsection {* Record package *}
    1.15  
    1.16 -use "Tools/quickcheck_record.ML"
    1.17  use "Tools/record.ML" setup Record.setup
    1.18  
    1.19  hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd