66 ("take_Nil", "take ?n [] = []"), |
66 ("take_Nil", "take ?n [] = []"), |
67 ("take_Cons", "take ?n (?x # ?xs) = (case ?n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> ?x # take m ?xs)"), |
67 ("take_Cons", "take ?n (?x # ?xs) = (case ?n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> ?x # take m ?xs)"), |
68 ("if_True", "(if True then ?x else ?y) = ?x"), |
68 ("if_True", "(if True then ?x else ?y) = ?x"), |
69 ("if_False", "(if False then ?x else ?y) = ?y"), |
69 ("if_False", "(if False then ?x else ?y) = ?y"), |
70 (*###*)("sym_real_mult_minus1", "- ?z1 = -1 * ?z1"), |
70 (*###*)("sym_real_mult_minus1", "- ?z1 = -1 * ?z1"), |
71 ("left_distrib", "(?a + ?b) * ?c = ?a * ?c + ?b * ?c"), |
71 ("distrib_right", "(?a + ?b) * ?c = ?a * ?c + ?b * ?c"), |
72 ("right_distrib", "?a * (?b + ?c) = ?a * ?b + ?a * ?c"), |
72 ("distrib_left", "?a * (?b + ?c) = ?a * ?b + ?a * ?c"), |
73 (*###*)(sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2"), |
73 (*###*)(sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2"), |
74 (*###*)(sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)"), |
74 (*###*)(sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)"), |
75 ("mult_1_right", "?a * 1 = ?a"), |
75 ("mult_1_right", "?a * 1 = ?a"), |
76 (*###*)(sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1"), |
76 (*###*)(sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1"), |
77 ("mult_1_left", "1 * ?a = ?a"), |
77 ("mult_1_left", "1 * ?a = ?a"), |
295 ("List.take_Nil", (prop_of o num_str) @{thm take_Nil}), |
295 ("List.take_Nil", (prop_of o num_str) @{thm take_Nil}), |
296 ("List.take_Cons", (prop_of o num_str) @{thm take_Cons}), |
296 ("List.take_Cons", (prop_of o num_str) @{thm take_Cons}), |
297 ("List.if_True", (prop_of o num_str) @{thm if_True}), |
297 ("List.if_True", (prop_of o num_str) @{thm if_True}), |
298 ("HOL.if_False", (prop_of o num_str) @{thm if_False}), |
298 ("HOL.if_False", (prop_of o num_str) @{thm if_False}), |
299 (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*) |
299 (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*) |
300 ("Rings.semiring_class.left_distrib", (prop_of o num_str) @{thm left_distrib}), |
300 ("Rings.semiring_class.distrib_right", (prop_of o num_str) @{thm distrib_right}), |
301 ("Rings.semiring_class.right_distrib", (prop_of o num_str) @{thm right_distrib}), |
301 ("Rings.semiring_class.distrib_left", (prop_of o num_str) @{thm distrib_left}), |
302 (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*) |
302 (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*) |
303 (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*) |
303 (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*) |
304 ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}), |
304 ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}), |
305 (*("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1")*) |
305 (*("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1")*) |
306 ("Groups.monoid_mult_class.mult_1_left", (prop_of o num_str) @{thm mult_1_left}), |
306 ("Groups.monoid_mult_class.mult_1_left", (prop_of o num_str) @{thm mult_1_left}), |
360 *** insert: preserved ["Isabelle","List","Theorems","take_Nil"] |
360 *** insert: preserved ["Isabelle","List","Theorems","take_Nil"] |
361 *** insert: preserved ["Isabelle","List","Theorems","take_Cons"] |
361 *** insert: preserved ["Isabelle","List","Theorems","take_Cons"] |
362 *** insert: preserved ["Isabelle","List","Theorems","if_True"] |
362 *** insert: preserved ["Isabelle","List","Theorems","if_True"] |
363 Thm.get_name_hint @{t^^^^^^True} = "HOL.if_True"; |
363 Thm.get_name_hint @{t^^^^^^True} = "HOL.if_True"; |
364 *** insert: preserved ["Isabelle","HOL","Theorems","if_False"] |
364 *** insert: preserved ["Isabelle","HOL","Theorems","if_False"] |
365 *** insert: preserved ["Isabelle","Rings","Theorems","left_distrib"] |
365 *** insert: preserved ["Isabelle","Rings","Theorems","distrib_right"] |
366 *** insert: preserved ["Isabelle","Rings","Theorems","right_distrib"] |
366 *** insert: preserved ["Isabelle","Rings","Theorems","distrib_left"] |
367 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_right"] |
367 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_right"] |
368 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_left"] |
368 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_left"] |
369 *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_left"] |
369 *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_left"] |
370 *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_right"] |
370 *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_right"] |
371 *** insert: preserved ["Isabelle","Groups","Theorems","add_0_left"] |
371 *** insert: preserved ["Isabelle","Groups","Theorems","add_0_left"] |