src/HOL/Inductive.thy
author oheimb
Sat, 15 Feb 1997 17:48:19 +0100
changeset 2636 4b30dbe4a020
parent 1862 74d4ae2f6fc3
child 5102 8c782c25a11e
permissions -rw-r--r--
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss, safe_asm_more_full_simp_ta, clasimpset HOL_css with modification functions new addss (old version retained as unsafe_addss), new Addss (old version retained as Unsafe_Addss), new auto_tac (old version retained as unsafe_auto_tac),

Inductive = Gfp + Prod + Sum + "indrule"