--- a/src/HOL/Bali/Basis.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Basis.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,13 +1,13 @@
(* Title: HOL/Bali/Basis.thy
Author: David von Oheimb
*)
-header {* Definitions extending HOL as logical basis of Bali *}
+subsection {* Definitions extending HOL as logical basis of Bali *}
theory Basis
imports Main "~~/src/HOL/Library/Old_Recdef"
begin
-section "misc"
+subsubsection "misc"
ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
@@ -109,7 +109,7 @@
done
-section "pairs"
+subsubsection "pairs"
lemma surjective_pairing5:
"p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))),
@@ -125,7 +125,7 @@
by (induct l) auto
-section "quantifiers"
+subsubsection "quantifiers"
lemma All_Ex_refl_eq2 [simp]: "(\<forall>x. (\<exists>b. x = f b \<and> Q b) \<longrightarrow> P x) = (\<forall>b. Q b \<longrightarrow> P (f b))"
by auto
@@ -143,7 +143,7 @@
by auto
-section "sums"
+subsubsection "sums"
notation case_sum (infixr "'(+')" 80)
@@ -186,7 +186,7 @@
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
-section "quantifiers for option type"
+subsubsection "quantifiers for option type"
syntax
"_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3! _:_:/ _)" [0,0,10] 10)
@@ -201,7 +201,7 @@
"\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST set_option A. P"
-section "Special map update"
+subsubsection "Special map update"
text{* Deemed too special for theory Map. *}
@@ -218,7 +218,7 @@
by (auto simp: chg_map_def)
-section "unique association lists"
+subsubsection "unique association lists"
definition unique :: "('a \<times> 'b) list \<Rightarrow> bool"
where "unique = distinct \<circ> map fst"
@@ -250,7 +250,7 @@
by (induct l) auto
-section "list patterns"
+subsubsection "list patterns"
definition lsplit :: "[['a, 'a list] \<Rightarrow> 'b, 'a list] \<Rightarrow> 'b"
where "lsplit = (\<lambda>f l. f (hd l) (tl l))"