author wenzelm
Fri, 03 Nov 2000 21:33:15 +0100
changeset 10386 581a5a143994
parent 10261 bb2f1e859177
child 10519 ade64af4c57c
permissions -rw-r--r--
provide case names for rev_induct, rev_cases;

(*theory Main includes everything; note that theory
  PreList already includes most HOL theories*)

theory Main = Map + String:

(*belongs to theory List*)
declare lists_mono [mono]
declare map_cong [recdef_cong]
lemmas rev_induct [case_names Nil snoc] = rev_induct
  and rev_cases [case_names Nil snoc] = rev_exhaust