# HG changeset patch # User wenzelm # Date 1259937036 -3600 # Node ID 406d8e34a3cf3c0d2afdddf1723bcfbcc0906e45 # Parent 29b928d32203f73798990ba62507ddd54ec17dce# Parent 78c0842510cbb248518f8ef9bee34a9a4be3f29e merged, resolving minor conflict, and recovering sane state; diff -r 78c0842510cb -r 406d8e34a3cf .hgtags --- a/.hgtags Fri Dec 04 14:34:24 2009 +0100 +++ b/.hgtags Fri Dec 04 15:30:36 2009 +0100 @@ -24,9 +24,4 @@ f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94 fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009 -9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test -9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test -4328de748fb2ceffe4ad5a6d5fbf3347f6aecfa6 isa2009-1-test -14ff44e21bec0e1b99d0f7322949b4fd012333e0 isa2009-1-test -14ff44e21bec0e1b99d0f7322949b4fd012333e0 isa2009-1-test -e1c262952b0285fa93f2e153891bc573d3de0f33 isa2009-1-test +6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1 diff -r 78c0842510cb -r 406d8e34a3cf Admin/makedist --- a/Admin/makedist Fri Dec 04 14:34:24 2009 +0100 +++ b/Admin/makedist Fri Dec 04 15:30:36 2009 +0100 @@ -4,7 +4,7 @@ ## global settings -REPOS_NAME="isabelle-release" +REPOS_NAME="isabelle" REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}" DISTPREFIX=${DISTPREFIX:-~/tmp/isadist} diff -r 78c0842510cb -r 406d8e34a3cf CONTRIBUTORS --- a/CONTRIBUTORS Fri Dec 04 14:34:24 2009 +0100 +++ b/CONTRIBUTORS Fri Dec 04 15:30:36 2009 +0100 @@ -3,6 +3,9 @@ who is listed as an author in one of the source files of this Isabelle distribution. +Contributions to this Isabelle version +-------------------------------------- + Contributions to Isabelle2009-1 ------------------------------- diff -r 78c0842510cb -r 406d8e34a3cf NEWS --- a/NEWS Fri Dec 04 14:34:24 2009 +0100 +++ b/NEWS Fri Dec 04 15:30:36 2009 +0100 @@ -1,6 +1,10 @@ Isabelle NEWS -- history user-relevant changes ============================================== +New in this Isabelle version +---------------------------- + + New in Isabelle2009-1 (December 2009) ------------------------------------- diff -r 78c0842510cb -r 406d8e34a3cf doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Fri Dec 04 14:34:24 2009 +0100 +++ b/doc-src/System/Thy/Basics.thy Fri Dec 04 15:30:36 2009 +0100 @@ -298,6 +298,10 @@ @{setting ISABELLE_HOME_USER} is included in the same manner (if that directory exists). Thus users can easily add private components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}. + + It is also possible to initialize components programmatically via + the \verb,init_component, shell function, say within the + \verb,settings, script of another component. *} diff -r 78c0842510cb -r 406d8e34a3cf doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Fri Dec 04 14:34:24 2009 +0100 +++ b/doc-src/System/Thy/document/Basics.tex Fri Dec 04 15:30:36 2009 +0100 @@ -308,7 +308,11 @@ itself. After initializing all of its sub-components recursively, \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} is included in the same manner (if that directory exists). Thus users can easily add private - components to \verb|$ISABELLE_HOME_USER/etc/components|.% + components to \verb|$ISABELLE_HOME_USER/etc/components|. + + It is also possible to initialize components programmatically via + the \verb,init_component, shell function, say within the + \verb,settings, script of another component.% \end{isamarkuptext}% \isamarkuptrue% % diff -r 78c0842510cb -r 406d8e34a3cf src/HOL/GCD.thy --- a/src/HOL/GCD.thy Fri Dec 04 14:34:24 2009 +0100 +++ b/src/HOL/GCD.thy Fri Dec 04 15:30:36 2009 +0100 @@ -779,14 +779,6 @@ apply auto done -lemma coprime_divprod_nat: "(d::nat) dvd a * b \ coprime d a \ d dvd b" - using coprime_dvd_mult_iff_nat[of d a b] - by (auto simp add: mult_commute) - -lemma coprime_divprod_int: "(d::int) dvd a * b \ coprime d a \ d dvd b" - using coprime_dvd_mult_iff_int[of d a b] - by (auto simp add: mult_commute) - lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c" shows "\b' c'. a = b' * c' \ b' dvd b \ c' dvd c" proof- diff -r 78c0842510cb -r 406d8e34a3cf src/HOL/Library/Crude_Executable_Set.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Crude_Executable_Set.thy Fri Dec 04 15:30:36 2009 +0100 @@ -0,0 +1,259 @@ +(* Title: HOL/Library/Crude_Executable_Set.thy + Author: Florian Haftmann, TU Muenchen +*) + +header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *} + +theory Crude_Executable_Set +imports List_Set +begin + +declare mem_def [code del] +declare Collect_def [code del] +declare insert_code [code del] +declare vimage_code [code del] + +subsection {* Set representation *} + +setup {* + Code.add_type_cmd "set" +*} + +definition Set :: "'a list \ 'a set" where + [simp]: "Set = set" + +definition Coset :: "'a list \ 'a set" where + [simp]: "Coset xs = - set xs" + +setup {* + Code.add_signature_cmd ("Set", "'a list \ 'a set") + #> Code.add_signature_cmd ("Coset", "'a list \ 'a set") + #> Code.add_signature_cmd ("set", "'a list \ 'a set") + #> Code.add_signature_cmd ("op \", "'a \ 'a set \ bool") +*} + +code_datatype Set Coset + + +subsection {* Basic operations *} + +lemma [code]: + "set xs = Set (remdups xs)" + by simp + +lemma [code]: + "x \ Set xs \ member x xs" + "x \ Coset xs \ \ member x xs" + by (simp_all add: mem_iff) + +definition is_empty :: "'a set \ bool" where + [simp]: "is_empty A \ A = {}" + +lemma [code_inline]: + "A = {} \ is_empty A" + by simp + +definition empty :: "'a set" where + [simp]: "empty = {}" + +lemma [code_inline]: + "{} = empty" + by simp + +setup {* + Code.add_signature_cmd ("is_empty", "'a set \ bool") + #> Code.add_signature_cmd ("empty", "'a set") + #> Code.add_signature_cmd ("insert", "'a \ 'a set \ 'a set") + #> Code.add_signature_cmd ("List_Set.remove", "'a \ 'a set \ 'a set") + #> Code.add_signature_cmd ("image", "('a \ 'b) \ 'a set \ 'b set") + #> Code.add_signature_cmd ("List_Set.project", "('a \ bool) \ 'a set \ 'a set") + #> Code.add_signature_cmd ("Ball", "'a set \ ('a \ bool) \ bool") + #> Code.add_signature_cmd ("Bex", "'a set \ ('a \ bool) \ bool") + #> Code.add_signature_cmd ("card", "'a set \ nat") +*} + +lemma is_empty_Set [code]: + "is_empty (Set xs) \ null xs" + by (simp add: empty_null) + +lemma empty_Set [code]: + "empty = Set []" + by simp + +lemma insert_Set [code]: + "insert x (Set xs) = Set (List_Set.insert x xs)" + "insert x (Coset xs) = Coset (remove_all x xs)" + by (simp_all add: insert_set insert_set_compl) + +lemma remove_Set [code]: + "remove x (Set xs) = Set (remove_all x xs)" + "remove x (Coset xs) = Coset (List_Set.insert x xs)" + by (simp_all add:remove_set remove_set_compl) + +lemma image_Set [code]: + "image f (Set xs) = Set (remdups (map f xs))" + by simp + +lemma project_Set [code]: + "project P (Set xs) = Set (filter P xs)" + by (simp add: project_set) + +lemma Ball_Set [code]: + "Ball (Set xs) P \ list_all P xs" + by (simp add: ball_set) + +lemma Bex_Set [code]: + "Bex (Set xs) P \ list_ex P xs" + by (simp add: bex_set) + +lemma card_Set [code]: + "card (Set xs) = length (remdups xs)" +proof - + have "card (set (remdups xs)) = length (remdups xs)" + by (rule distinct_card) simp + then show ?thesis by simp +qed + + +subsection {* Derived operations *} + +definition set_eq :: "'a set \ 'a set \ bool" where + [simp]: "set_eq = op =" + +lemma [code_inline]: + "op = = set_eq" + by simp + +definition subset_eq :: "'a set \ 'a set \ bool" where + [simp]: "subset_eq = op \" + +lemma [code_inline]: + "op \ = subset_eq" + by simp + +definition subset :: "'a set \ 'a set \ bool" where + [simp]: "subset = op \" + +lemma [code_inline]: + "op \ = subset" + by simp + +setup {* + Code.add_signature_cmd ("set_eq", "'a set \ 'a set \ bool") + #> Code.add_signature_cmd ("subset_eq", "'a set \ 'a set \ bool") + #> Code.add_signature_cmd ("subset", "'a set \ 'a set \ bool") +*} + +lemma set_eq_subset_eq [code]: + "set_eq A B \ subset_eq A B \ subset_eq B A" + by auto + +lemma subset_eq_forall [code]: + "subset_eq A B \ (\x\A. x \ B)" + by (simp add: subset_eq) + +lemma subset_subset_eq [code]: + "subset A B \ subset_eq A B \ \ subset_eq B A" + by (simp add: subset) + + +subsection {* Functorial operations *} + +definition inter :: "'a set \ 'a set \ 'a set" where + [simp]: "inter = op \" + +lemma [code_inline]: + "op \ = inter" + by simp + +definition subtract :: "'a set \ 'a set \ 'a set" where + [simp]: "subtract A B = B - A" + +lemma [code_inline]: + "B - A = subtract A B" + by simp + +definition union :: "'a set \ 'a set \ 'a set" where + [simp]: "union = op \" + +lemma [code_inline]: + "op \ = union" + by simp + +definition Inf :: "'a::complete_lattice set \ 'a" where + [simp]: "Inf = Complete_Lattice.Inf" + +lemma [code_inline]: + "Complete_Lattice.Inf = Inf" + by simp + +definition Sup :: "'a::complete_lattice set \ 'a" where + [simp]: "Sup = Complete_Lattice.Sup" + +lemma [code_inline]: + "Complete_Lattice.Sup = Sup" + by simp + +definition Inter :: "'a set set \ 'a set" where + [simp]: "Inter = Inf" + +lemma [code_inline]: + "Inf = Inter" + by simp + +definition Union :: "'a set set \ 'a set" where + [simp]: "Union = Sup" + +lemma [code_inline]: + "Sup = Union" + by simp + +setup {* + Code.add_signature_cmd ("inter", "'a set \ 'a set \ 'a set") + #> Code.add_signature_cmd ("subtract", "'a set \ 'a set \ 'a set") + #> Code.add_signature_cmd ("union", "'a set \ 'a set \ 'a set") + #> Code.add_signature_cmd ("Inf", "'a set \ 'a") + #> Code.add_signature_cmd ("Sup", "'a set \ 'a") + #> Code.add_signature_cmd ("Inter", "'a set set \ 'a set") + #> Code.add_signature_cmd ("Union", "'a set set \ 'a set") +*} + +lemma inter_project [code]: + "inter A (Set xs) = Set (List.filter (\x. x \ A) xs)" + "inter A (Coset xs) = foldl (\A x. remove x A) A xs" + by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set) + +lemma subtract_remove [code]: + "subtract (Set xs) A = foldl (\A x. remove x A) A xs" + "subtract (Coset xs) A = Set (List.filter (\x. x \ A) xs)" + by (auto simp add: minus_set) + +lemma union_insert [code]: + "union (Set xs) A = foldl (\A x. insert x A) A xs" + "union (Coset xs) A = Coset (List.filter (\x. x \ A) xs)" + by (auto simp add: union_set) + +lemma Inf_inf [code]: + "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs" + "Inf (Coset []) = (bot :: 'a::complete_lattice)" + by (simp_all add: Inf_Univ bot_def [symmetric] Inf_set_fold) + +lemma Sup_sup [code]: + "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs" + "Sup (Coset []) = (top :: 'a::complete_lattice)" + by (simp_all add: Sup_Univ top_def [symmetric] Sup_set_fold) + +lemma Inter_inter [code]: + "Inter (Set xs) = foldl inter (Coset []) xs" + "Inter (Coset []) = empty" + unfolding Inter_def Inf_inf by simp_all + +lemma Union_union [code]: + "Union (Set xs) = foldl union empty xs" + "Union (Coset []) = Coset []" + unfolding Union_def Sup_sup by simp_all + +hide (open) const is_empty empty remove + set_eq subset_eq subset inter union subtract Inf Sup Inter Union + +end diff -r 78c0842510cb -r 406d8e34a3cf src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Fri Dec 04 14:34:24 2009 +0100 +++ b/src/HOL/Library/Fset.thy Fri Dec 04 15:30:36 2009 +0100 @@ -210,7 +210,7 @@ member (foldl (\B A. Fset (member B \ A)) (Coset []) (List.map member As))" by (rule foldl_apply_inv) simp then show "Inter (Set As) = foldl inter (Coset []) As" - by (simp add: Inter_set image_set inter inter_def_raw foldl_map) + by (simp add: Inf_set_fold image_set inter inter_def_raw foldl_map) show "Inter (Coset []) = empty" by simp qed @@ -229,7 +229,7 @@ member (foldl (\B A. Fset (member B \ A)) empty (List.map member As))" by (rule foldl_apply_inv) simp then show "Union (Set As) = foldl union empty As" - by (simp add: Union_set image_set union_def_raw foldl_map) + by (simp add: Sup_set_fold image_set union_def_raw foldl_map) show "Union (Coset []) = Coset []" by simp qed diff -r 78c0842510cb -r 406d8e34a3cf src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Fri Dec 04 14:34:24 2009 +0100 +++ b/src/HOL/Library/Library.thy Fri Dec 04 15:30:36 2009 +0100 @@ -14,6 +14,7 @@ Continuity ContNotDenum Countable + Crude_Executable_Set Diagonalize Efficient_Nat Enum diff -r 78c0842510cb -r 406d8e34a3cf src/HOL/Library/List_Set.thy --- a/src/HOL/Library/List_Set.thy Fri Dec 04 14:34:24 2009 +0100 +++ b/src/HOL/Library/List_Set.thy Fri Dec 04 15:30:36 2009 +0100 @@ -85,6 +85,50 @@ "project P (set xs) = set (filter P xs)" by (auto simp add: project_def) +text {* FIXME move the following to @{text Finite_Set.thy} *} + +lemma fun_left_comm_idem_inf: + "fun_left_comm_idem inf" +proof +qed (auto simp add: inf_left_commute) + +lemma fun_left_comm_idem_sup: + "fun_left_comm_idem sup" +proof +qed (auto simp add: sup_left_commute) + +lemma inf_Inf_fold_inf: + fixes A :: "'a::complete_lattice set" + assumes "finite A" + shows "inf B (Inf A) = fold inf B A" +proof - + interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf) + from `finite A` show ?thesis by (induct A arbitrary: B) + (simp_all add: top_def [symmetric] Inf_insert inf_commute fold_fun_comm) +qed + +lemma sup_Sup_fold_sup: + fixes A :: "'a::complete_lattice set" + assumes "finite A" + shows "sup B (Sup A) = fold sup B A" +proof - + interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup) + from `finite A` show ?thesis by (induct A arbitrary: B) + (simp_all add: bot_def [symmetric] Sup_insert sup_commute fold_fun_comm) +qed + +lemma Inf_fold_inf: + fixes A :: "'a::complete_lattice set" + assumes "finite A" + shows "Inf A = fold inf top A" + using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2) + +lemma Sup_fold_sup: + fixes A :: "'a::complete_lattice set" + assumes "finite A" + shows "Sup A = fold sup bot A" + using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2) + subsection {* Functorial set operations *} @@ -105,41 +149,13 @@ by (simp add: minus_fold_remove [of _ A] fold_set) qed -lemma Inter_set: - "Inter (set As) = foldl (op \) UNIV As" -proof - - have "fold (op \) UNIV (set As) = foldl (\y x. x \ y) UNIV As" - by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - then show ?thesis - by (simp only: Inter_fold_inter finite_set Int_commute) -qed - -lemma Union_set: - "Union (set As) = foldl (op \) {} As" -proof - - have "fold (op \) {} (set As) = foldl (\y x. x \ y) {} As" - by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - then show ?thesis - by (simp only: Union_fold_union finite_set Un_commute) -qed +lemma INFI_set_fold: -- "FIXME move to List.thy" + "INFI (set xs) f = foldl (\y x. inf (f x) y) top xs" + unfolding INFI_def image_set Inf_set_fold foldl_map by (simp add: inf_commute) -lemma INTER_set: - "INTER (set As) f = foldl (\B A. f A \ B) UNIV As" -proof - - have "fold (\A. op \ (f A)) UNIV (set As) = foldl (\B A. f A \ B) UNIV As" - by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - then show ?thesis - by (simp only: INTER_fold_inter finite_set) -qed - -lemma UNION_set: - "UNION (set As) f = foldl (\B A. f A \ B) {} As" -proof - - have "fold (\A. op \ (f A)) {} (set As) = foldl (\B A. f A \ B) {} As" - by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - then show ?thesis - by (simp only: UNION_fold_union finite_set) -qed +lemma SUPR_set_fold: -- "FIXME move to List.thy" + "SUPR (set xs) f = foldl (\y x. sup (f x) y) bot xs" + unfolding SUPR_def image_set Sup_set_fold foldl_map by (simp add: sup_commute) subsection {* Derived set operations *} diff -r 78c0842510cb -r 406d8e34a3cf src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Fri Dec 04 14:34:24 2009 +0100 +++ b/src/HOL/Number_Theory/Primes.thy Fri Dec 04 15:30:36 2009 +0100 @@ -360,16 +360,15 @@ from prime_dvd_mult_nat[OF p pab'] have "p dvd a \ p dvd b" . moreover - {assume pa: "p dvd a" - have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) + { assume pa: "p dvd a" from coprime_common_divisor_nat [OF ab, OF pa] p have "\ p dvd b" by auto with p have "coprime b p" by (subst gcd_commute_nat, intro prime_imp_coprime_nat) hence pnb: "coprime (p^n) b" by (subst gcd_commute_nat, rule coprime_exp_nat) - from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast } + from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast } moreover - {assume pb: "p dvd b" + { assume pb: "p dvd b" have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) from coprime_common_divisor_nat [OF ab, of p] pb p have "\ p dvd a" by auto @@ -377,7 +376,7 @@ by (subst gcd_commute_nat, intro prime_imp_coprime_nat) hence pna: "coprime (p^n) a" by (subst gcd_commute_nat, rule coprime_exp_nat) - from coprime_divprod_nat[OF pab pna] have ?thesis by blast } + from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast } ultimately have ?thesis by blast} ultimately show ?thesis by blast qed diff -r 78c0842510cb -r 406d8e34a3cf src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Dec 04 14:34:24 2009 +0100 +++ b/src/HOL/Set.thy Fri Dec 04 15:30:36 2009 +0100 @@ -1556,6 +1556,9 @@ lemma imp_refl: "P --> P" .. +lemma not_mono: "Q --> P ==> ~ P --> ~ Q" + by iprover + lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)" by iprover @@ -1576,9 +1579,6 @@ lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c" by iprover -lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c" - by iprover - subsubsection {* Inverse image of a function *} @@ -1724,7 +1724,6 @@ val contra_subsetD = @{thm contra_subsetD} val distinct_lemma = @{thm distinct_lemma} val eq_to_mono = @{thm eq_to_mono} -val eq_to_mono2 = @{thm eq_to_mono2} val equalityCE = @{thm equalityCE} val equalityD1 = @{thm equalityD1} val equalityD2 = @{thm equalityD2} diff -r 78c0842510cb -r 406d8e34a3cf src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Fri Dec 04 14:34:24 2009 +0100 +++ b/src/HOL/Tools/sat_solver.ML Fri Dec 04 15:30:36 2009 +0100 @@ -311,7 +311,7 @@ fun int_from_string s = case Int.fromString s of SOME i => i - | NONE => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number") + | NONE => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number") (* int list -> int list list *) fun clauses xs = let @@ -350,7 +350,7 @@ o (map (map literal_from_int)) o clauses o (map int_from_string) - o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) + o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"]))) o filter_preamble o filter (fn l => l <> "") o split_lines diff -r 78c0842510cb -r 406d8e34a3cf src/Pure/General/xml.scala --- a/src/Pure/General/xml.scala Fri Dec 04 14:34:24 2009 +0100 +++ b/src/Pure/General/xml.scala Fri Dec 04 15:30:36 2009 +0100 @@ -86,18 +86,10 @@ } - /* document object model (DOM) */ - - def document(tree: Tree, styles: String*) = { - val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument - doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\"")) + /* document object model (W3C DOM) */ - for (style <- styles) { - doc.appendChild(doc.createProcessingInstruction("xml-stylesheet", - "href=\"" + style + "\" type=\"text/css\"")) - } - - // main body + def document_node(doc: Document, tree: Tree): Node = + { def DOM(tr: Tree): Node = tr match { case Elem(name, atts, ts) => { val node = doc.createElement(name) @@ -107,9 +99,21 @@ } case Text(txt) => doc.createTextNode(txt) } + DOM(tree) + } + + def document(tree: Tree, styles: String*): Document = + { + val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument + doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\"")) + + for (style <- styles) { + doc.appendChild(doc.createProcessingInstruction("xml-stylesheet", + "href=\"" + style + "\" type=\"text/css\"")) + } val root_elem = tree match { - case Elem(_, _, _) => DOM(tree) - case Text(_) => DOM(Elem(Markup.ROOT, Nil, List(tree))) + case Elem(_, _, _) => document_node(doc, tree) + case Text(_) => document_node(doc, (Elem(Markup.ROOT, Nil, List(tree)))) } doc.appendChild(root_elem) doc diff -r 78c0842510cb -r 406d8e34a3cf src/Pure/Isar/code.ML diff -r 78c0842510cb -r 406d8e34a3cf src/Pure/type.ML --- a/src/Pure/type.ML Fri Dec 04 14:34:24 2009 +0100 +++ b/src/Pure/type.ML Fri Dec 04 15:30:36 2009 +0100 @@ -19,6 +19,7 @@ types: decl Name_Space.table, log_types: string list} val empty_tsig: tsig + val build_tsig: (Name_Space.T * Sorts.algebra) * sort * decl Name_Space.table -> tsig val defaultS: tsig -> sort val logical_types: tsig -> string list val eq_sort: tsig -> sort * sort -> bool diff -r 78c0842510cb -r 406d8e34a3cf src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Fri Dec 04 14:34:24 2009 +0100 +++ b/src/Tools/Code/code_preproc.ML Fri Dec 04 15:30:36 2009 +0100 @@ -111,7 +111,7 @@ -- perhaps by means of upcoming code certificates with a corresponding preprocessor protocol*); -fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); +fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); fun eqn_conv conv = let @@ -148,7 +148,7 @@ in ct |> Simplifier.rewrite pre - |> rhs_conv (AxClass.unoverload_conv thy) + |> trans_conv_rule (AxClass.unoverload_conv thy) end; fun postprocess_conv thy ct = @@ -157,7 +157,7 @@ in ct |> AxClass.overload_conv thy - |> rhs_conv (Simplifier.rewrite post) + |> trans_conv_rule (Simplifier.rewrite post) end; fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);