--- a/src/HOL/IsaMakefile Mon Mar 26 21:00:23 2012 +0200
+++ b/src/HOL/IsaMakefile Mon Mar 26 21:00:39 2012 +0200
@@ -65,6 +65,7 @@
HOL-Predicate_Compile_Examples \
HOL-Prolog \
HOL-Proofs-ex \
+ HOL-Proofs-Lambda \
HOL-SET_Protocol \
HOL-SPARK-Examples \
HOL-SPARK-Manual \
@@ -80,8 +81,6 @@
HOL-ZF
# ^ this is the sort position
-# FIXME HOL-Proofs-Lambda
-
generate: \
HOL-HOL4-Generate \
HOL-HOL_Light-Generate
--- a/src/HOL/Library/Code_Integer.thy Mon Mar 26 21:00:23 2012 +0200
+++ b/src/HOL/Library/Code_Integer.thy Mon Mar 26 21:00:39 2012 +0200
@@ -16,11 +16,13 @@
"nat k = (if k \<le> 0 then 0 else
let
(l, j) = divmod_int k 2;
- l' = 2 * nat l
+ n = nat l;
+ l' = n + n
in if j = 0 then l' else Suc l')"
proof -
have "2 = nat 2" by simp
show ?thesis
+ apply (subst nat_mult_2 [symmetric])
apply (auto simp add: Let_def divmod_int_mod_div not_le
nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
apply (unfold `2 = nat 2`)
--- a/src/HOL/Num.thy Mon Mar 26 21:00:23 2012 +0200
+++ b/src/HOL/Num.thy Mon Mar 26 21:00:39 2012 +0200
@@ -1010,12 +1010,12 @@
subsection {* code module namespace *}
code_modulename SML
- Numeral Arith
+ Num Arith
code_modulename OCaml
- Numeral Arith
+ Num Arith
code_modulename Haskell
- Numeral Arith
+ Num Arith
end
--- a/src/HOL/Proofs/Lambda/Eta.thy Mon Mar 26 21:00:23 2012 +0200
+++ b/src/HOL/Proofs/Lambda/Eta.thy Mon Mar 26 21:00:39 2012 +0200
@@ -159,7 +159,7 @@
apply (slowsimp intro: rtrancl_eta_subst eta_subst)
apply (blast intro: rtrancl_eta_AppL)
apply (blast intro: rtrancl_eta_AppR)
- apply simp;
+ apply simp
apply (slowsimp intro: rtrancl_eta_Abs free_beta
iff del: dB.distinct simp: dB.distinct) (*23 seconds?*)
done