--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Sep 16 09:18:15 2011 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Sat Sep 17 03:37:14 2011 +0200
@@ -412,7 +412,6 @@
proof (rule antisym)
show "(SUP i. integral\<^isup>P M (?g i)) \<le> ?y"
using g_in_G
- using [[simp_trace]]
by (auto intro!: exI Sup_mono simp: SUP_def)
show "?y \<le> (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq
by (auto intro!: SUP_mono positive_integral_mono Max_ge)
--- a/src/HOL/Word/Bit_Int.thy Fri Sep 16 09:18:15 2011 +0200
+++ b/src/HOL/Word/Bit_Int.thy Sat Sep 17 03:37:14 2011 +0200
@@ -1,9 +1,9 @@
(*
Author: Jeremy Dawson and Gerwin Klein, NICTA
- definition and basic theorems for bit-wise logical operations
+ Definitions and basic theorems for bit-wise logical operations
for integers expressed using Pls, Min, BIT,
- and converting them to and from lists of bools
+ and converting them to and from lists of bools.
*)
header {* Bitwise Operations on Binary Integers *}
--- a/src/HOL/Word/Bit_Representation.thy Fri Sep 16 09:18:15 2011 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Sat Sep 17 03:37:14 2011 +0200
@@ -1,8 +1,7 @@
(*
Author: Jeremy Dawson, NICTA
- contains basic definition to do with integers
- expressed using Pls, Min, BIT
+ Basic definitions to do with integers, expressed using Pls, Min, BIT.
*)
header {* Basic Definitions for Binary Integers *}
@@ -876,8 +875,7 @@
size list = number_of k"
by (auto simp: pred_def succ_def split add : split_if_asm)
-lemmas ls_splits =
- prod.split split_split prod.split_asm split_split_asm split_if_asm
+lemmas ls_splits = prod.split prod.split_asm split_if_asm
lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)"
by (cases y) auto
--- a/src/HOL/Word/Bool_List_Representation.thy Fri Sep 16 09:18:15 2011 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Sat Sep 17 03:37:14 2011 +0200
@@ -1,7 +1,7 @@
(*
Author: Jeremy Dawson, NICTA
- contains theorems to do with integers, expressed using Pls, Min, BIT,
+ Theorems to do with integers, expressed using Pls, Min, BIT,
theorems linking them to lists of booleans, and repeated splitting
and concatenation.
*)
@@ -60,8 +60,10 @@
subsection "Arithmetic in terms of bool lists"
-(* arithmetic operations in terms of the reversed bool list,
- assuming input list(s) the same length, and don't extend them *)
+text {*
+ Arithmetic operations in terms of the reversed bool list,
+ assuming input list(s) the same length, and don't extend them.
+*}
primrec rbl_succ :: "bool list => bool list" where
Nil: "rbl_succ Nil = Nil"
@@ -72,13 +74,13 @@
| Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
primrec rbl_add :: "bool list => bool list => bool list" where
- (* result is length of first arg, second arg may be longer *)
+ -- "result is length of first arg, second arg may be longer"
Nil: "rbl_add Nil x = Nil"
| Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
(y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
primrec rbl_mult :: "bool list => bool list => bool list" where
- (* result is length of first arg, second arg may be longer *)
+ -- "result is length of first arg, second arg may be longer"
Nil: "rbl_mult Nil x = Nil"
| Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
if y then rbl_add ws x else ws)"
@@ -112,7 +114,7 @@
bin_to_bl_aux (n - 1) w (True # bl)"
by (cases n) auto
-(** link between bin and bool list **)
+text {* Link between bin and bool list. *}
lemma bl_to_bin_aux_append:
"bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
--- a/src/HOL/Word/Misc_Numeric.thy Fri Sep 16 09:18:15 2011 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Sat Sep 17 03:37:14 2011 +0200
@@ -11,13 +11,6 @@
lemma the_elemI: "y = {x} ==> the_elem y = x"
by simp
-lemmas split_split = prod.split
-lemmas split_split_asm = prod.split_asm
-lemmas split_splits = split_split split_split_asm
-
-lemmas funpow_0 = funpow.simps(1)
-lemmas funpow_Suc = funpow.simps(2)
-
lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto
lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by arith
--- a/src/HOL/Word/Misc_Typedef.thy Fri Sep 16 09:18:15 2011 +0200
+++ b/src/HOL/Word/Misc_Typedef.thy Sat Sep 17 03:37:14 2011 +0200
@@ -1,8 +1,7 @@
(*
- Author: Jeremy Dawson and Gerwin Klein, NICTA
+ Author: Jeremy Dawson and Gerwin Klein, NICTA
- consequences of type definition theorems,
- and of extended type definition theorems
+ Consequences of type definition theorems, and of extended type definition. theorems
*)
header {* Type Definition Theorems *}
--- a/src/HOL/Word/Word.thy Fri Sep 16 09:18:15 2011 +0200
+++ b/src/HOL/Word/Word.thy Sat Sep 17 03:37:14 2011 +0200
@@ -4514,7 +4514,7 @@
apply (simp add: mod_nat_add word_size)
done
-lemma word_neq_0_conv [simp]:
+lemma word_neq_0_conv:
fixes w :: "'a :: len word"
shows "(w \<noteq> 0) = (0 < w)"
proof -
--- a/src/Tools/Code/code_haskell.ML Fri Sep 16 09:18:15 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML Sat Sep 17 03:37:14 2011 +0200
@@ -17,13 +17,13 @@
val target = "Haskell";
val language_extensions =
- ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"];
+ ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"];
val language_pragma =
- "{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
+ "{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
val language_params =
- space_implode " " (map (prefix "-X") language_extensions);
+ space_implode " " (map (prefix "-X") language_extensions);
open Basic_Code_Thingol;
open Code_Printer;