# HG changeset patch # User huffman # Date 1321357169 -3600 # Node ID 6246bef495ff5c119b986d2c36967861d9178036 # Parent 697e387bb859c18a00af37b901f8e6fdfbe59301 avoid theorem references like 'semiring_norm(111)' diff -r 697e387bb859 -r 6246bef495ff src/HOL/Metis_Examples/Binary_Tree.thy --- a/src/HOL/Metis_Examples/Binary_Tree.thy Tue Nov 15 09:22:19 2011 +0100 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy Tue Nov 15 12:39:29 2011 +0100 @@ -264,7 +264,7 @@ "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" apply (induct t1) apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) - semiring_norm(111)) + Suc_eq_plus1) by (simp add: left_distrib) declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]] diff -r 697e387bb859 -r 6246bef495ff src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Nov 15 09:22:19 2011 +0100 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Nov 15 12:39:29 2011 +0100 @@ -107,6 +107,6 @@ by (metis_exhaust null_def) lemma "(0::nat) + 0 = 0" -by (metis_exhaust arithmetic_simps(38)) +by (metis_exhaust add_0_left) end