# HG changeset patch # User huffman # Date 1332785487 -7200 # Node ID bd1679890503fa1a119079b2f0dd30444b3a19aa # Parent d0d16b20b6cebaf0df046249f6116d61942f3010# Parent 24a1cb3fdf09fd8213474c92764b751ed79334d3 merged diff -r 24a1cb3fdf09 -r bd1679890503 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Mar 26 20:09:52 2012 +0200 +++ b/src/HOL/IsaMakefile Mon Mar 26 20:11:27 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 diff -r 24a1cb3fdf09 -r bd1679890503 src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Mon Mar 26 20:09:52 2012 +0200 +++ b/src/HOL/Library/Code_Integer.thy Mon Mar 26 20:11:27 2012 +0200 @@ -16,11 +16,13 @@ "nat k = (if k \ 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`) diff -r 24a1cb3fdf09 -r bd1679890503 src/HOL/Num.thy --- a/src/HOL/Num.thy Mon Mar 26 20:09:52 2012 +0200 +++ b/src/HOL/Num.thy Mon Mar 26 20:11:27 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 diff -r 24a1cb3fdf09 -r bd1679890503 src/HOL/Proofs/Lambda/Eta.thy --- a/src/HOL/Proofs/Lambda/Eta.thy Mon Mar 26 20:09:52 2012 +0200 +++ b/src/HOL/Proofs/Lambda/Eta.thy Mon Mar 26 20:11:27 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