replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
--- a/doc-src/Codegen/Thy/Program.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/Codegen/Thy/Program.thy Fri Apr 16 21:28:09 2010 +0200
@@ -430,7 +430,7 @@
subsection {* Inductive Predicates *}
(*<*)
-hide const append
+hide_const append
inductive append
where
--- a/doc-src/Locales/Locales/Examples.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/Locales/Locales/Examples.thy Fri Apr 16 21:28:09 2010 +0200
@@ -2,7 +2,7 @@
imports Main
begin
-hide %invisible const Lattices.lattice
+hide_const %invisible Lattices.lattice
pretty_setmargin %invisible 65
(*
--- a/doc-src/Locales/Locales/document/Examples.tex Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/Locales/Locales/document/Examples.tex Fri Apr 16 21:28:09 2010 +0200
@@ -25,8 +25,8 @@
\endisadeliminvisible
%
\isataginvisible
-\isacommand{hide}\isamarkupfalse%
-\ const\ Lattices{\isachardot}lattice\isanewline
+\isacommand{hide{\isacharunderscore}const}\isamarkupfalse%
+\ Lattices{\isachardot}lattice\isanewline
\isacommand{pretty{\isacharunderscore}setmargin}\isamarkupfalse%
\ {\isadigit{6}}{\isadigit{5}}%
\endisataginvisible
--- a/doc-src/TutorialI/Datatype/Nested.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Apr 16 21:28:09 2010 +0200
@@ -11,7 +11,7 @@
Consider the following model of terms
where function symbols can be applied to a list of arguments:
*}
-(*<*)hide const Var(*>*)
+(*<*)hide_const Var(*>*)
datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
text{*\noindent
--- a/doc-src/TutorialI/Documents/Documents.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy Fri Apr 16 21:28:09 2010 +0200
@@ -138,7 +138,7 @@
*}
(*<*)
-hide const xor
+hide_const xor
setup {* Sign.add_path "version1" *}
(*>*)
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
@@ -161,7 +161,7 @@
*}
(*<*)
-hide const xor
+hide_const xor
setup {* Sign.add_path "version2" *}
(*>*)
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60)
--- a/doc-src/TutorialI/Misc/Option2.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy Fri Apr 16 21:28:09 2010 +0200
@@ -1,7 +1,7 @@
(*<*)
theory Option2 imports Main begin
-hide const None Some
-hide type option
+hide_const None Some
+hide_type option
(*>*)
text{*\indexbold{*option (type)}\indexbold{*None (constant)}%
--- a/doc-src/TutorialI/Types/Overloading.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy Fri Apr 16 21:28:09 2010 +0200
@@ -1,6 +1,6 @@
(*<*)theory Overloading imports Main Setup begin
-hide (open) "class" plus (*>*)
+hide_class (open) plus (*>*)
text {* Type classes allow \emph{overloading}; thus a constant may
have multiple definitions at non-overlapping types. *}
--- a/src/FOL/FOL.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/FOL/FOL.thy Fri Apr 16 21:28:09 2010 +0200
@@ -371,7 +371,7 @@
lemmas induct_rulify_fallback =
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
-hide const induct_forall induct_implies induct_equal induct_conj
+hide_const induct_forall induct_implies induct_equal induct_conj
text {* Method setup. *}
--- a/src/HOL/Bali/Basis.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Bali/Basis.thy Fri Apr 16 21:28:09 2010 +0200
@@ -176,7 +176,7 @@
section "sums"
-hide const In0 In1
+hide_const In0 In1
notation sum_case (infixr "'(+')"80)
--- a/src/HOL/Bali/TypeSafe.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Fri Apr 16 21:28:09 2010 +0200
@@ -9,7 +9,7 @@
section "error free"
-hide const field
+hide_const field
lemma error_free_halloc:
assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
--- a/src/HOL/Code_Evaluation.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Fri Apr 16 21:28:09 2010 +0200
@@ -280,8 +280,8 @@
end
*}
-hide const dummy_term App valapp
-hide (open) const Const termify valtermify term_of term_of_num
+hide_const dummy_term App valapp
+hide_const (open) Const termify valtermify term_of term_of_num
subsection {* Tracing of generated and evaluated code *}
@@ -301,7 +301,7 @@
code_const "tracing :: String.literal => 'a => 'a"
(Eval "Code'_Evaluation.tracing")
-hide (open) const tracing
+hide_const (open) tracing
code_reserved Eval Code_Evaluation
subsection {* Evaluation setup *}
--- a/src/HOL/Code_Numeral.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Code_Numeral.thy Fri Apr 16 21:28:09 2010 +0200
@@ -278,7 +278,7 @@
then show ?thesis by (auto simp add: int_of_def mult_ac)
qed
-hide (open) const of_nat nat_of int_of
+hide_const (open) of_nat nat_of int_of
subsubsection {* Lazy Evaluation of an indexed function *}
@@ -289,7 +289,7 @@
termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
-hide (open) const iterate_upto
+hide_const (open) iterate_upto
subsection {* Code generator setup *}
--- a/src/HOL/DSequence.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/DSequence.thy Fri Apr 16 21:28:09 2010 +0200
@@ -97,13 +97,13 @@
code_reserved Eval DSequence
(*
-hide type Sequence.seq
+hide_type Sequence.seq
-hide const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
+hide_const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
*)
-hide (open) const empty single eval map_seq bind union if_seq not_seq map
-hide (open) fact empty_def single_def eval.simps map_seq.simps bind_def union_def
+hide_const (open) empty single eval map_seq bind union if_seq not_seq map
+hide_fact (open) empty_def single_def eval.simps map_seq.simps bind_def union_def
if_seq_def not_seq_def map_def
end
--- a/src/HOL/Datatype.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Datatype.thy Fri Apr 16 21:28:09 2010 +0200
@@ -512,8 +512,8 @@
text {* hides popular names *}
-hide (open) type node item
-hide (open) const Push Node Atom Leaf Numb Lim Split Case
+hide_type (open) node item
+hide_const (open) Push Node Atom Leaf Numb Lim Split Case
use "Tools/Datatype/datatype.ML"
--- a/src/HOL/Finite_Set.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Finite_Set.thy Fri Apr 16 21:28:09 2010 +0200
@@ -513,7 +513,7 @@
class finite =
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
setup {* Sign.parent_path *}
-hide const finite
+hide_const finite
context finite
begin
--- a/src/HOL/Fun.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Fun.thy Fri Apr 16 21:28:09 2010 +0200
@@ -525,7 +525,7 @@
lemma bij_swap_iff: "bij (swap a b f) = bij f"
by (simp add: bij_def)
-hide (open) const swap
+hide_const (open) swap
subsection {* Inversion of injective functions *}
--- a/src/HOL/Groups.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Groups.thy Fri Apr 16 21:28:09 2010 +0200
@@ -88,7 +88,7 @@
class one =
fixes one :: 'a ("1")
-hide (open) const zero one
+hide_const (open) zero one
syntax
"_index1" :: index ("\<^sub>1")
--- a/src/HOL/HOL.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/HOL.thy Fri Apr 16 21:28:09 2010 +0200
@@ -1567,7 +1567,7 @@
lemma [induct_simp]: "(x = x) = True"
by (rule simp_thms)
-hide const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
+hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
use "~~/src/Tools/induct_tacs.ML"
setup InductTacs.setup
@@ -1886,8 +1886,8 @@
Nbe.add_const_alias @{thm equals_alias_cert}
*}
-hide (open) const eq
-hide const eq
+hide_const (open) eq
+hide_const eq
text {* Cases *}
--- a/src/HOL/Imperative_HOL/Array.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Fri Apr 16 21:28:09 2010 +0200
@@ -92,7 +92,7 @@
return a
done)"
-hide (open) const new map -- {* avoid clashed with some popular names *}
+hide_const (open) new map -- {* avoid clashed with some popular names *}
subsection {* Properties *}
@@ -115,28 +115,28 @@
definition new' where
[code del]: "new' = Array.new o Code_Numeral.nat_of"
-hide (open) const new'
+hide_const (open) new'
lemma [code]:
"Array.new = Array.new' o Code_Numeral.of_nat"
by (simp add: new'_def o_def)
definition of_list' where
[code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
-hide (open) const of_list'
+hide_const (open) of_list'
lemma [code]:
"Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
by (simp add: of_list'_def)
definition make' where
[code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
-hide (open) const make'
+hide_const (open) make'
lemma [code]:
"Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
by (simp add: make'_def o_def)
definition length' where
[code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
-hide (open) const length'
+hide_const (open) length'
lemma [code]:
"Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
by (simp add: length'_def monad_simp',
@@ -145,14 +145,14 @@
definition nth' where
[code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
-hide (open) const nth'
+hide_const (open) nth'
lemma [code]:
"Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
by (simp add: nth'_def)
definition upd' where
[code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
-hide (open) const upd'
+hide_const (open) upd'
lemma [code]:
"Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
by (simp add: upd'_def monad_simp upd_return)
--- a/src/HOL/Imperative_HOL/Heap.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Fri Apr 16 21:28:09 2010 +0200
@@ -432,6 +432,6 @@
"array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
by (simp add: array_present_def new_ref_def ref_def Let_def)
-hide (open) const empty array array_of_list upd length ref
+hide_const (open) empty array array_of_list upd length ref
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Apr 16 21:28:09 2010 +0200
@@ -405,7 +405,7 @@
lemmas MREC_rule = mrec.MREC_rule
lemmas MREC_pinduct = mrec.MREC_pinduct
-hide (open) const heap execute
+hide_const (open) heap execute
subsection {* Code generator setup *}
@@ -426,7 +426,7 @@
"raise s = raise_exc (Fail (STR s))"
unfolding Fail_def raise_exc_def raise_def ..
-hide (open) const Fail raise_exc
+hide_const (open) Fail raise_exc
subsubsection {* SML and OCaml *}
--- a/src/HOL/Imperative_HOL/Ref.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Fri Apr 16 21:28:09 2010 +0200
@@ -41,7 +41,7 @@
return y
done)"
-hide (open) const new lookup update change
+hide_const (open) new lookup update change
subsection {* Properties *}
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Fri Apr 16 21:28:09 2010 +0200
@@ -8,7 +8,7 @@
imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray
begin
-hide (open) const swap rev
+hide_const (open) swap rev
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
"swap a i j = (do
--- a/src/HOL/Int.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Int.thy Fri Apr 16 21:28:09 2010 +0200
@@ -2263,7 +2263,7 @@
lemma [code]: "nat i = nat_aux i 0"
by (simp add: nat_aux_def)
-hide (open) const nat_aux
+hide_const (open) nat_aux
lemma zero_is_num_zero [code, code_unfold_post]:
"(0\<Colon>int) = Numeral0"
@@ -2325,7 +2325,7 @@
quickcheck_params [default_type = int]
-hide (open) const Pls Min Bit0 Bit1 succ pred
+hide_const (open) Pls Min Bit0 Bit1 succ pred
subsection {* Legacy theorems *}
--- a/src/HOL/Lattice/Bounds.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Lattice/Bounds.thy Fri Apr 16 21:28:09 2010 +0200
@@ -6,7 +6,7 @@
theory Bounds imports Orders begin
-hide (open) const inf sup
+hide_const (open) inf sup
subsection {* Infimum and supremum *}
--- a/src/HOL/Lazy_Sequence.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy Fri Apr 16 21:28:09 2010 +0200
@@ -212,8 +212,8 @@
where
"hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
-hide (open) type lazy_sequence
-hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
-hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
+hide_type (open) lazy_sequence
+hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
+hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
end
--- a/src/HOL/Library/Dlist.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Fri Apr 16 21:28:09 2010 +0200
@@ -247,6 +247,6 @@
end
-hide (open) const member fold empty insert remove map filter null member length fold
+hide_const (open) member fold empty insert remove map filter null member length fold
end
--- a/src/HOL/Library/Efficient_Nat.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Apr 16 21:28:09 2010 +0200
@@ -496,6 +496,6 @@
code_modulename Haskell
Efficient_Nat Arith
-hide const int
+hide_const int
end
--- a/src/HOL/Library/Executable_Set.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Executable_Set.thy Fri Apr 16 21:28:09 2010 +0200
@@ -265,7 +265,7 @@
"Union (Coset []) = Coset []"
unfolding Union_def Sup_sup by simp_all
-hide (open) const is_empty empty remove
+hide_const (open) is_empty empty remove
set_eq subset_eq subset inter union subtract Inf Sup Inter Union
end
--- a/src/HOL/Library/Fset.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Fset.thy Fri Apr 16 21:28:09 2010 +0200
@@ -293,7 +293,7 @@
declare mem_def [simp del]
-hide (open) const is_empty insert remove map filter forall exists card
+hide_const (open) is_empty insert remove map filter forall exists card
Inter Union
end
--- a/src/HOL/Library/Mapping.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Fri Apr 16 21:28:09 2010 +0200
@@ -146,6 +146,6 @@
by (cases m) simp
-hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
+hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
end
\ No newline at end of file
--- a/src/HOL/Library/Multiset.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Apr 16 21:28:09 2010 +0200
@@ -1001,7 +1001,7 @@
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
-hide (open) const bagify
+hide_const (open) bagify
subsection {* The multiset order *}
--- a/src/HOL/Library/Nested_Environment.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Nested_Environment.thy Fri Apr 16 21:28:09 2010 +0200
@@ -54,7 +54,7 @@
| "lookup_option None xs = None"
| "lookup_option (Some e) xs = lookup e xs"
-hide const lookup_option
+hide_const lookup_option
text {*
\medskip The characteristic cases of @{term lookup} are expressed by
@@ -262,7 +262,7 @@
| "update_option xs opt (Some e) =
(if xs = [] then opt else Some (update xs opt e))"
-hide const update_option
+hide_const update_option
text {*
\medskip The characteristic cases of @{term update} are expressed by
--- a/src/HOL/Library/RBT.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/RBT.thy Fri Apr 16 21:28:09 2010 +0200
@@ -224,7 +224,7 @@
"HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
by (simp add: eq Mapping_def entries_lookup)
-hide (open) const impl_of lookup empty insert delete
+hide_const (open) impl_of lookup empty insert delete
entries keys bulkload map_entry map fold
(*>*)
--- a/src/HOL/Library/RBT_Impl.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Fri Apr 16 21:28:09 2010 +0200
@@ -1079,6 +1079,6 @@
then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
qed
-hide (open) const Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
+hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
end
--- a/src/HOL/Library/Transitive_Closure_Table.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri Apr 16 21:28:09 2010 +0200
@@ -227,8 +227,8 @@
value "test\<^sup>*\<^sup>* A C"
value "test\<^sup>*\<^sup>* C A"
-hide type ty
-hide const test A B C
+hide_type ty
+hide_const test A B C
end
--- a/src/HOL/List.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/List.thy Fri Apr 16 21:28:09 2010 +0200
@@ -172,7 +172,8 @@
insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"insert x xs = (if x \<in> set xs then xs else x # xs)"
-hide (open) const insert hide (open) fact insert_def
+hide_const (open) insert
+hide_fact (open) insert_def
primrec
remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -4584,7 +4585,7 @@
declare set_map [symmetric, code_unfold]
-hide (open) const length_unique
+hide_const (open) length_unique
text {* Code for bounded quantification and summation over nats. *}
--- a/src/HOL/NSA/Filter.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/NSA/Filter.thy Fri Apr 16 21:28:09 2010 +0200
@@ -403,6 +403,6 @@
lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
-hide (open) const filter
+hide_const (open) filter
end
--- a/src/HOL/Nat.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Nat.thy Fri Apr 16 21:28:09 2010 +0200
@@ -175,7 +175,7 @@
end
-hide (open) fact add_0 add_0_right diff_0
+hide_fact (open) add_0 add_0_right diff_0
instantiation nat :: comm_semiring_1_cancel
begin
@@ -1212,7 +1212,7 @@
"funpow (Suc n) f = f o funpow n f"
unfolding funpow_code_def by simp_all
-hide (open) const funpow
+hide_const (open) funpow
lemma funpow_add:
"f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
@@ -1504,7 +1504,7 @@
lemma diff_diff_eq: "[| k \<le> m; k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
by (simp split add: nat_diff_split)
-hide (open) fact diff_diff_eq
+hide_fact (open) diff_diff_eq
lemma eq_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
by (auto split add: nat_diff_split)
--- a/src/HOL/New_DSequence.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/New_DSequence.thy Fri Apr 16 21:28:09 2010 +0200
@@ -91,12 +91,12 @@
None => Lazy_Sequence.hb_single ()
| Some ((), xq) => Lazy_Sequence.empty)"
-hide (open) type pos_dseq neg_dseq
+hide_type (open) pos_dseq neg_dseq
-hide (open) const
+hide_const (open)
pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
-hide (open) fact
+hide_fact (open)
pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def
neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
--- a/src/HOL/New_Random_Sequence.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/New_Random_Sequence.thy Fri Apr 16 21:28:09 2010 +0200
@@ -91,16 +91,16 @@
where
"neg_map f P = neg_bind P (neg_single o f)"
(*
-hide const DSequence.empty DSequence.single DSequence.eval
+hide_const DSequence.empty DSequence.single DSequence.eval
DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
DSequence.map
*)
-hide (open) const
+hide_const (open)
pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
-hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
+hide_type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
(* FIXME: hide facts *)
-(*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
+(*hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
end
\ No newline at end of file
--- a/src/HOL/Nitpick.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Nitpick.thy Fri Apr 16 21:28:09 2010 +0200
@@ -237,15 +237,15 @@
setup {* Nitpick_Isar.setup *}
-hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
+hide_const (open) unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl'
wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
less_eq_frac of_frac
-hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
+hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
word
-hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
+hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
--- a/src/HOL/Option.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Option.thy Fri Apr 16 21:28:09 2010 +0200
@@ -82,7 +82,7 @@
by (rule ext) (simp split: sum.split)
-hide (open) const set map
+hide_const (open) set map
subsubsection {* Code generator setup *}
@@ -102,7 +102,7 @@
"eq_class.eq x None \<longleftrightarrow> is_none x"
by (simp add: eq is_none_none)
-hide (open) const is_none
+hide_const (open) is_none
code_type option
(SML "_ option")
--- a/src/HOL/Predicate.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Predicate.thy Fri Apr 16 21:28:09 2010 +0200
@@ -934,8 +934,8 @@
bot ("\<bottom>") and
bind (infixl "\<guillemotright>=" 70)
-hide (open) type pred seq
-hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
+hide_type (open) pred seq
+hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
end
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Fri Apr 16 21:28:09 2010 +0200
@@ -1168,7 +1168,7 @@
code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
-hide const a b
+hide_const a b
subsection {* Lambda *}
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Fri Apr 16 21:28:09 2010 +0200
@@ -150,7 +150,7 @@
quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
oops
-hide const a b
+hide_const a b
subsection {* Lexicographic order *}
(* TODO *)
--- a/src/HOL/Product_Type.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Product_Type.thy Fri Apr 16 21:28:09 2010 +0200
@@ -637,7 +637,7 @@
use "Tools/split_rule.ML"
setup Split_Rule.setup
-hide const internal_split
+hide_const internal_split
lemmas prod_caseI = prod.cases [THEN iffD2, standard]
--- a/src/HOL/Quickcheck.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Quickcheck.thy Fri Apr 16 21:28:09 2010 +0200
@@ -203,9 +203,9 @@
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
where "map f P = bind P (single o f)"
-hide (open) fact iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
-hide (open) type randompred
-hide (open) const random collapse beyond random_fun_aux random_fun_lift
+hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
+hide_type (open) randompred
+hide_const (open) random collapse beyond random_fun_aux random_fun_lift
iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
end
--- a/src/HOL/Random.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Random.thy Fri Apr 16 21:28:09 2010 +0200
@@ -174,10 +174,10 @@
end;
*}
-hide (open) type seed
-hide (open) const inc_shift minus_shift log "next" split_seed
+hide_type (open) seed
+hide_const (open) inc_shift minus_shift log "next" split_seed
iterate range select pick select_weight
-hide (open) fact range_def
+hide_fact (open) range_def
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Random_Sequence.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Random_Sequence.thy Fri Apr 16 21:28:09 2010 +0200
@@ -48,14 +48,14 @@
"map f P = bind P (single o f)"
(*
-hide const DSequence.empty DSequence.single DSequence.eval
+hide_const DSequence.empty DSequence.single DSequence.eval
DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
DSequence.map
*)
-hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
+hide_const (open) empty single bind union if_random_dseq not_random_dseq Random map
-hide type DSequence.dseq random_dseq
-hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
+hide_type DSequence.dseq random_dseq
+hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
end
\ No newline at end of file
--- a/src/HOL/Record.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Record.thy Fri Apr 16 21:28:09 2010 +0200
@@ -455,7 +455,7 @@
use "Tools/record.ML"
setup Record.setup
-hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
+hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
iso_tuple_update_accessor_eq_assist tuple_iso_tuple
--- a/src/HOL/String.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/String.thy Fri Apr 16 21:28:09 2010 +0200
@@ -217,6 +217,6 @@
in Codegen.add_codegen "char_codegen" char_codegen end
*}
-hide (open) type literal
+hide_type (open) literal
end
\ No newline at end of file
--- a/src/HOL/Sum_Type.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Sum_Type.thy Fri Apr 16 21:28:09 2010 +0200
@@ -187,6 +187,6 @@
show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
qed
-hide (open) const Suml Sumr Projl Projr
+hide_const (open) Suml Sumr Projl Projr
end
--- a/src/HOL/Typerep.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Typerep.thy Fri Apr 16 21:28:09 2010 +0200
@@ -90,6 +90,6 @@
code_reserved Eval Term
-hide (open) const typerep Typerep
+hide_const (open) typerep Typerep
end
--- a/src/HOL/Word/BinGeneral.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Word/BinGeneral.thy Fri Apr 16 21:28:09 2010 +0200
@@ -28,7 +28,7 @@
lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
-hide (open) const B0 B1
+hide_const (open) B0 B1
lemma Min_ne_Pls [iff]:
"Int.Min ~= Int.Pls"
--- a/src/HOL/ex/Meson_Test.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy Fri Apr 16 21:28:09 2010 +0200
@@ -16,7 +16,7 @@
below and constants declared in HOL!
*}
-hide (open) const subset member quotient union inter
+hide_const (open) subset member quotient union inter
text {*
Test data for the MESON proof procedure
--- a/src/HOL/ex/Numeral.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Fri Apr 16 21:28:09 2010 +0200
@@ -879,7 +879,7 @@
declare zero_is_num_zero [code_unfold del]
declare one_is_num_one [code_unfold del]
-hide (open) const sub dup
+hide_const (open) sub dup
subsection {* Numeral equations as default simplification rules *}
--- a/src/HOL/ex/RPred.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/ex/RPred.thy Fri Apr 16 21:28:09 2010 +0200
@@ -47,6 +47,6 @@
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
where "map f P = bind P (return o f)"
-hide (open) const return bind supp map
+hide_const (open) return bind supp map
end
\ No newline at end of file
--- a/src/HOL/ex/SVC_Oracle.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Apr 16 21:28:09 2010 +0200
@@ -17,7 +17,7 @@
iff_keep :: "[bool, bool] => bool"
iff_unfold :: "[bool, bool] => bool"
-hide const iff_keep iff_unfold
+hide_const iff_keep iff_unfold
oracle svc_oracle = Svc.oracle
--- a/src/HOLCF/Fixrec.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOLCF/Fixrec.thy Fri Apr 16 21:28:09 2010 +0200
@@ -608,7 +608,7 @@
(@{const_name UU}, @{const_name match_UU}) ]
*}
-hide (open) const return bind fail run cases
+hide_const (open) return bind fail run cases
lemmas [fixrec_simp] =
run_strict run_fail run_return
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Fri Apr 16 21:28:09 2010 +0200
@@ -59,7 +59,7 @@
(* hiding and restricting *)
hide_asig :: "['a signature, 'a set] => 'a signature"
- "hide" :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+ hide :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
restrict_asig :: "['a signature, 'a set] => 'a signature"
restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
--- a/src/HOLCF/Universal.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOLCF/Universal.thy Fri Apr 16 21:28:09 2010 +0200
@@ -809,7 +809,7 @@
apply (rule ubasis_until_less)
done
-hide (open) const
+hide_const (open)
node
choose
choose_pos
--- a/src/Pure/Isar/isar_cmd.ML Fri Apr 16 20:56:40 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Apr 16 21:28:09 2010 +0200
@@ -20,7 +20,10 @@
val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
local_theory -> local_theory
- val hide_names: bool -> string * xstring list -> theory -> theory
+ val hide_class: bool -> xstring list -> theory -> theory
+ val hide_type: bool -> xstring list -> theory -> theory
+ val hide_const: bool -> xstring list -> theory -> theory
+ val hide_fact: bool -> xstring list -> theory -> theory
val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
@@ -202,23 +205,19 @@
(* hide names *)
-val hide_kinds =
- [("class", (Sign.intern_class, can o Sign.certify_class, Sign.hide_class)),
- ("type", (Sign.intern_type, Sign.declared_tyname, Sign.hide_type)),
- ("const", (Sign.intern_const, Sign.declared_const, Sign.hide_const)),
- ("fact", (PureThy.intern_fact, PureThy.defined_fact, PureThy.hide_fact))];
+fun hide_names intern check hide fully xnames thy =
+ let
+ val names = map (intern thy) xnames;
+ val bads = filter_out (check thy) names;
+ in
+ if null bads then fold (hide fully) names thy
+ else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
+ end;
-fun hide_names b (kind, xnames) thy =
- (case AList.lookup (op =) hide_kinds kind of
- SOME (intern, check, hide) =>
- let
- val names = map (intern thy) xnames;
- val bads = filter_out (check thy) names;
- in
- if null bads then fold (hide b) names thy
- else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
- end
- | NONE => error ("Bad name space specification: " ^ quote kind));
+val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
+val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
+val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
+val hide_fact = hide_names PureThy.intern_fact PureThy.defined_fact PureThy.hide_fact;
(* goals *)
--- a/src/Pure/Isar/isar_syn.ML Fri Apr 16 20:56:40 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Apr 16 21:28:09 2010 +0200
@@ -285,10 +285,15 @@
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
(Scan.succeed (Toplevel.theory Sign.local_path));
-val _ =
- OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
- ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
- (Toplevel.theory o uncurry IsarCmd.hide_names));
+fun hide_names name hide what =
+ OuterSyntax.command name ("hide " ^ what ^ " from name space") K.thy_decl
+ ((P.opt_keyword "open" >> not) -- Scan.repeat1 P.xname >>
+ (Toplevel.theory o uncurry hide));
+
+val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
+val _ = hide_names "hide_type" IsarCmd.hide_type "types";
+val _ = hide_names "hide_const" IsarCmd.hide_const "constants";
+val _ = hide_names "hide_fact" IsarCmd.hide_fact "facts";
(* use ML text *)