moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
authorhaftmann
Thu Apr 19 19:36:24 2012 +0200 (2012-04-19)
changeset 476571ba213363d0c
parent 47656 d6a3b69f4404
child 47658 7631f6f7873d
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
src/HOL/HOL.thy
src/Tools/Code_Generator.thy
     1.1 --- a/src/HOL/HOL.thy	Sat Apr 21 15:26:05 2012 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Apr 19 19:36:24 2012 +0200
     1.3 @@ -7,16 +7,19 @@
     1.4  theory HOL
     1.5  imports Pure "~~/src/Tools/Code_Generator"
     1.6  keywords
     1.7 -  "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag
     1.8 +  "try" "solve_direct" "quickcheck"
     1.9 +    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and
    1.10 +  "quickcheck_params" :: thy_decl
    1.11  uses
    1.12    ("Tools/hologic.ML")
    1.13 +  "~~/src/Tools/misc_legacy.ML"
    1.14 +  "~~/src/Tools/try.ML"
    1.15 +  "~~/src/Tools/quickcheck.ML"
    1.16 +  "~~/src/Tools/solve_direct.ML"
    1.17    "~~/src/Tools/IsaPlanner/zipper.ML"
    1.18    "~~/src/Tools/IsaPlanner/isand.ML"
    1.19    "~~/src/Tools/IsaPlanner/rw_tools.ML"
    1.20    "~~/src/Tools/IsaPlanner/rw_inst.ML"
    1.21 -  "~~/src/Tools/intuitionistic.ML"
    1.22 -  "~~/src/Tools/project_rule.ML"
    1.23 -  "~~/src/Tools/cong_tac.ML"
    1.24    "~~/src/Provers/hypsubst.ML"
    1.25    "~~/src/Provers/splitter.ML"
    1.26    "~~/src/Provers/classical.ML"
    1.27 @@ -28,6 +31,9 @@
    1.28    ("Tools/simpdata.ML")
    1.29    "~~/src/Tools/atomize_elim.ML"
    1.30    "~~/src/Tools/induct.ML"
    1.31 +  "~~/src/Tools/cong_tac.ML"
    1.32 +  "~~/src/Tools/intuitionistic.ML"
    1.33 +  "~~/src/Tools/project_rule.ML"
    1.34    ("~~/src/Tools/induction.ML")
    1.35    ("~~/src/Tools/induct_tacs.ML")
    1.36    ("Tools/cnf_funcs.ML")
    1.37 @@ -35,10 +41,13 @@
    1.38    "~~/src/Tools/case_product.ML"
    1.39  begin
    1.40  
    1.41 -setup {* Intuitionistic.method_setup @{binding iprover} *}
    1.42 -setup Subtyping.setup
    1.43 -setup Case_Product.setup
    1.44 -
    1.45 +setup {*
    1.46 +  Intuitionistic.method_setup @{binding iprover}
    1.47 +  #> Quickcheck.setup
    1.48 +  #> Solve_Direct.setup
    1.49 +  #> Subtyping.setup
    1.50 +  #> Case_Product.setup
    1.51 +*}
    1.52  
    1.53  subsection {* Primitive logic *}
    1.54  
    1.55 @@ -2008,3 +2017,4 @@
    1.56  hide_const (open) eq equal
    1.57  
    1.58  end
    1.59 +
     2.1 --- a/src/Tools/Code_Generator.thy	Sat Apr 21 15:26:05 2012 +0200
     2.2 +++ b/src/Tools/Code_Generator.thy	Thu Apr 19 19:36:24 2012 +0200
     2.3 @@ -7,19 +7,14 @@
     2.4  theory Code_Generator
     2.5  imports Pure
     2.6  keywords
     2.7 -  "try" "solve_direct" "quickcheck" "value" "print_codeproc"
     2.8 -    "code_thms" "code_deps" "export_code" :: diag and
     2.9 -  "quickcheck_params" "code_class" "code_instance" "code_type"
    2.10 +  "value" "print_codeproc" "code_thms" "code_deps" "export_code" :: diag and
    2.11 +  "code_class" "code_instance" "code_type"
    2.12      "code_const" "code_reserved" "code_include" "code_modulename"
    2.13      "code_abort" "code_monad" "code_reflect" :: thy_decl and
    2.14    "datatypes" "functions" "module_name" "file" "checking"
    2.15  uses
    2.16 -  "~~/src/Tools/misc_legacy.ML"
    2.17 +  "~~/src/Tools/value.ML"
    2.18    "~~/src/Tools/cache_io.ML"
    2.19 -  "~~/src/Tools/try.ML"
    2.20 -  "~~/src/Tools/solve_direct.ML"
    2.21 -  "~~/src/Tools/quickcheck.ML"
    2.22 -  "~~/src/Tools/value.ML"
    2.23    "~~/src/Tools/Code/code_preproc.ML"
    2.24    "~~/src/Tools/Code/code_thingol.ML"
    2.25    "~~/src/Tools/Code/code_simp.ML"
    2.26 @@ -34,15 +29,13 @@
    2.27  begin
    2.28  
    2.29  setup {*
    2.30 -  Solve_Direct.setup
    2.31 +  Value.setup
    2.32    #> Code_Preproc.setup
    2.33    #> Code_Simp.setup
    2.34    #> Code_Target.setup
    2.35    #> Code_ML.setup
    2.36    #> Code_Haskell.setup
    2.37    #> Code_Scala.setup
    2.38 -  #> Quickcheck.setup
    2.39 -  #> Value.setup
    2.40  *}
    2.41  
    2.42  code_datatype "TYPE('a\<Colon>{})"
    2.43 @@ -80,3 +73,4 @@
    2.44  hide_const (open) holds
    2.45  
    2.46  end
    2.47 +