src/HOL/Tools/Lifting/lifting_setup.ML
changeset 50214 67fb9a168d10
parent 50176 701747176952
child 50231 81a067b188b8
equal deleted inserted replaced
50213:7b73c0509835 50214:67fb9a168d10
   264 val opt_gen_code =
   264 val opt_gen_code =
   265   Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true
   265   Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true
   266 
   266 
   267 val _ = 
   267 val _ = 
   268   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
   268   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
   269     "Setup lifting infrastructure" 
   269     "setup lifting infrastructure" 
   270       (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
   270       (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
   271         (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
   271         (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
   272 end;
   272 end;