replaced skolem declarations by automatic skolemization of everything
authorpaulson
Fri Aug 25 18:44:59 2006 +0200 (2006-08-25)
changeset 20414029c4f9dc6f4
parent 20413 5a6e152a7114
child 20415 e3d2d7b01279
replaced skolem declarations by automatic skolemization of everything
src/HOL/Main.thy
     1.1 --- a/src/HOL/Main.thy	Fri Aug 25 00:10:10 2006 +0200
     1.2 +++ b/src/HOL/Main.thy	Fri Aug 25 18:44:59 2006 +0200
     1.3 @@ -13,94 +13,9 @@
     1.4    PreList} already includes most HOL theories.
     1.5  *}
     1.6  
     1.7 -text {* \medskip Late clause setup: installs \emph{all} simprules and
     1.8 -  claset rules into the clause cache; cf.\ theory @{text
     1.9 -  Reconstruction}. *}
    1.10 +text {* \medskip Late clause setup: installs \emph{all} known theorems
    1.11 +  into the clause cache; cf.\ theory @{text Reconstruction}. *}
    1.12  
    1.13  setup ResAxioms.setup
    1.14  
    1.15 -
    1.16 -(*The following declarations generate polymorphic Skolem functions for 
    1.17 -  these theorems. NOTE: We need an automatic mechanism to ensure that this
    1.18 -  happens for all theorems stored in descendant theories.*)
    1.19 -
    1.20 -(*HOL*)
    1.21 -declare ext [skolem]
    1.22 -
    1.23 -(*Finite_Set*)
    1.24 -declare setprod_nonneg [skolem]
    1.25 -declare setprod_pos [skolem]
    1.26 -declare setsum_bounded [skolem]
    1.27 -declare setsum_mono [skolem]
    1.28 -declare setsum_nonneg [skolem]
    1.29 -declare setsum_nonpos [skolem]
    1.30 -declare setsum_0' [skolem]
    1.31 -declare setprod_1' [skolem]
    1.32 -
    1.33 -declare Fun.image_INT [skolem]
    1.34 -
    1.35 -(*List. Only none look useful.*)
    1.36 -declare Cons_eq_append_conv [skolem]
    1.37 -declare Cons_eq_map_D [skolem]
    1.38 -declare Cons_eq_map_conv [skolem]
    1.39 -declare append_eq_Cons_conv [skolem]
    1.40 -declare map_eq_Cons_D [skolem]
    1.41 -declare map_eq_Cons_conv [skolem]
    1.42 -
    1.43 -declare Orderings.max_leastL [skolem]
    1.44 -declare Orderings.max_leastR [skolem]
    1.45 -
    1.46 -declare Product_Type.Sigma_mono [skolem]
    1.47 -
    1.48 -(*Relation*)
    1.49 -declare Domain_iff [skolem]
    1.50 -declare Image_iff [skolem]
    1.51 -declare Range_iff [skolem]
    1.52 -declare antisym_def [skolem]
    1.53 -declare reflI [skolem]
    1.54 -declare rel_compEpair [skolem]
    1.55 -declare refl_def [skolem]
    1.56 -declare sym_def [skolem]
    1.57 -declare trans_def [skolem]
    1.58 -declare single_valued_def [skolem]  
    1.59 -
    1.60 -(*Relation_Power*)
    1.61 -declare rel_pow_E2 [skolem]
    1.62 -declare rel_pow_E [skolem]
    1.63 -declare rel_pow_Suc_D2 [skolem]
    1.64 -declare rel_pow_Suc_D2' [skolem]
    1.65 -declare rel_pow_Suc_E [skolem]
    1.66 -
    1.67 -(*Set*)
    1.68 -declare Collect_mono [skolem]
    1.69 -declare INT_anti_mono [skolem]
    1.70 -declare INT_greatest [skolem]
    1.71 -declare INT_subset_iff [skolem]
    1.72 -declare Int_Collect_mono [skolem]
    1.73 -declare Inter_greatest[skolem]
    1.74 -declare UN_least [skolem]
    1.75 -declare UN_mono [skolem]
    1.76 -declare UN_subset_iff [skolem]
    1.77 -declare Union_least [skolem]
    1.78 -declare Union_disjoint [skolem]
    1.79 -declare disjoint_iff_not_equal [skolem]
    1.80 -declare image_subsetI [skolem]
    1.81 -declare image_subset_iff [skolem]
    1.82 -declare subset_def [skolem]
    1.83 -declare subset_iff [skolem]
    1.84 -
    1.85 -(*Transitive_Closure*)
    1.86 -declare converse_rtranclE [skolem]
    1.87 -declare irrefl_trancl_rD [skolem]
    1.88 -declare rtranclE [skolem]
    1.89 -declare tranclD [skolem]
    1.90 -declare tranclE [skolem]
    1.91 -
    1.92 -(*Wellfounded_Recursion*)
    1.93 -declare acyclicI [skolem]
    1.94 -declare acyclic_def [skolem]
    1.95 -declare wfI [skolem]
    1.96 -declare wf_def [skolem]
    1.97 -declare wf_eq_minimal [skolem]
    1.98 -
    1.99  end