src/HOL/HOL.thy
changeset 30240 5b25fee0362c
parent 30238 d8944fd4365e
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/HOL.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -12,14 +12,15 @@
     1.4    "~~/src/Tools/IsaPlanner/isand.ML"
     1.5    "~~/src/Tools/IsaPlanner/rw_tools.ML"
     1.6    "~~/src/Tools/IsaPlanner/rw_inst.ML"
     1.7 -  "~~/src/Provers/project_rule.ML"
     1.8 +  "~~/src/Tools/intuitionistic.ML"
     1.9 +  "~~/src/Tools/project_rule.ML"
    1.10    "~~/src/Provers/hypsubst.ML"
    1.11    "~~/src/Provers/splitter.ML"
    1.12    "~~/src/Provers/classical.ML"
    1.13    "~~/src/Provers/blast.ML"
    1.14    "~~/src/Provers/clasimp.ML"
    1.15 -  "~~/src/Provers/coherent.ML"
    1.16 -  "~~/src/Provers/eqsubst.ML"
    1.17 +  "~~/src/Tools/coherent.ML"
    1.18 +  "~~/src/Tools/eqsubst.ML"
    1.19    "~~/src/Provers/quantifier1.ML"
    1.20    ("Tools/simpdata.ML")
    1.21    "~~/src/Tools/random_word.ML"
    1.22 @@ -28,7 +29,8 @@
    1.23    ("~~/src/Tools/induct_tacs.ML")
    1.24    "~~/src/Tools/value.ML"
    1.25    "~~/src/Tools/code/code_name.ML"
    1.26 -  "~~/src/Tools/code/code_funcgr.ML"
    1.27 +  "~~/src/Tools/code/code_funcgr.ML" (*formal dependency*)
    1.28 +  "~~/src/Tools/code/code_wellsorted.ML" 
    1.29    "~~/src/Tools/code/code_thingol.ML"
    1.30    "~~/src/Tools/code/code_printer.ML"
    1.31    "~~/src/Tools/code/code_target.ML"
    1.32 @@ -38,6 +40,9 @@
    1.33    ("Tools/recfun_codegen.ML")
    1.34  begin
    1.35  
    1.36 +setup {* Intuitionistic.method_setup "iprover" *}
    1.37 +
    1.38 +
    1.39  subsection {* Primitive logic *}
    1.40  
    1.41  subsubsection {* Core syntax *}
    1.42 @@ -290,7 +295,7 @@
    1.43  typed_print_translation {*
    1.44  let
    1.45    fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    1.46 -    if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
    1.47 +    if (not o null) ts orelse T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
    1.48      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    1.49  in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
    1.50  *} -- {* show types that are presumably too general *}
    1.51 @@ -1704,11 +1709,6 @@
    1.52  subsection {* Nitpick theorem store *}
    1.53  
    1.54  ML {*
    1.55 -structure Nitpick_Const_Def_Thms = NamedThmsFun
    1.56 -(
    1.57 -  val name = "nitpick_const_def"
    1.58 -  val description = "pseudo-definition of constants as needed by Nitpick"
    1.59 -)
    1.60  structure Nitpick_Const_Simp_Thms = NamedThmsFun
    1.61  (
    1.62    val name = "nitpick_const_simp"
    1.63 @@ -1725,8 +1725,7 @@
    1.64    val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
    1.65  )
    1.66  *}
    1.67 -setup {* Nitpick_Const_Def_Thms.setup
    1.68 -         #> Nitpick_Const_Simp_Thms.setup
    1.69 +setup {* Nitpick_Const_Simp_Thms.setup
    1.70           #> Nitpick_Const_Psimp_Thms.setup
    1.71           #> Nitpick_Ind_Intro_Thms.setup *}
    1.72