# HG changeset patch
# User paulson
# Date 1156524299 -7200
# Node ID 029c4f9dc6f42ffe73373914a61da5d875dcf746
# Parent  5a6e152a71144a9384d6e6043e5f80350239ee77
replaced skolem declarations by automatic skolemization of everything

diff -r 5a6e152a7114 -r 029c4f9dc6f4 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Aug 25 00:10:10 2006 +0200
+++ b/src/HOL/Main.thy	Fri Aug 25 18:44:59 2006 +0200
@@ -13,94 +13,9 @@
   PreList} already includes most HOL theories.
 *}
 
-text {* \medskip Late clause setup: installs \emph{all} simprules and
-  claset rules into the clause cache; cf.\ theory @{text
-  Reconstruction}. *}
+text {* \medskip Late clause setup: installs \emph{all} known theorems
+  into the clause cache; cf.\ theory @{text Reconstruction}. *}
 
 setup ResAxioms.setup
 
-
-(*The following declarations generate polymorphic Skolem functions for 
-  these theorems. NOTE: We need an automatic mechanism to ensure that this
-  happens for all theorems stored in descendant theories.*)
-
-(*HOL*)
-declare ext [skolem]
-
-(*Finite_Set*)
-declare setprod_nonneg [skolem]
-declare setprod_pos [skolem]
-declare setsum_bounded [skolem]
-declare setsum_mono [skolem]
-declare setsum_nonneg [skolem]
-declare setsum_nonpos [skolem]
-declare setsum_0' [skolem]
-declare setprod_1' [skolem]
-
-declare Fun.image_INT [skolem]
-
-(*List. Only none look useful.*)
-declare Cons_eq_append_conv [skolem]
-declare Cons_eq_map_D [skolem]
-declare Cons_eq_map_conv [skolem]
-declare append_eq_Cons_conv [skolem]
-declare map_eq_Cons_D [skolem]
-declare map_eq_Cons_conv [skolem]
-
-declare Orderings.max_leastL [skolem]
-declare Orderings.max_leastR [skolem]
-
-declare Product_Type.Sigma_mono [skolem]
-
-(*Relation*)
-declare Domain_iff [skolem]
-declare Image_iff [skolem]
-declare Range_iff [skolem]
-declare antisym_def [skolem]
-declare reflI [skolem]
-declare rel_compEpair [skolem]
-declare refl_def [skolem]
-declare sym_def [skolem]
-declare trans_def [skolem]
-declare single_valued_def [skolem]  
-
-(*Relation_Power*)
-declare rel_pow_E2 [skolem]
-declare rel_pow_E [skolem]
-declare rel_pow_Suc_D2 [skolem]
-declare rel_pow_Suc_D2' [skolem]
-declare rel_pow_Suc_E [skolem]
-
-(*Set*)
-declare Collect_mono [skolem]
-declare INT_anti_mono [skolem]
-declare INT_greatest [skolem]
-declare INT_subset_iff [skolem]
-declare Int_Collect_mono [skolem]
-declare Inter_greatest[skolem]
-declare UN_least [skolem]
-declare UN_mono [skolem]
-declare UN_subset_iff [skolem]
-declare Union_least [skolem]
-declare Union_disjoint [skolem]
-declare disjoint_iff_not_equal [skolem]
-declare image_subsetI [skolem]
-declare image_subset_iff [skolem]
-declare subset_def [skolem]
-declare subset_iff [skolem]
-
-(*Transitive_Closure*)
-declare converse_rtranclE [skolem]
-declare irrefl_trancl_rD [skolem]
-declare rtranclE [skolem]
-declare tranclD [skolem]
-declare tranclE [skolem]
-
-(*Wellfounded_Recursion*)
-declare acyclicI [skolem]
-declare acyclic_def [skolem]
-declare wfI [skolem]
-declare wf_def [skolem]
-declare wf_eq_minimal [skolem]
-
 end