src/HOL/HOL.thy
changeset 47657 1ba213363d0c
parent 46973 d68798000e46
child 48073 1b609a7837ef
     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 +