src/HOL/Main.thy

New function complete_split_rule for complete splitting of partially
splitted rules (as generated by inductive definition package).

(*  Title:      HOL/Main.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000 TU Muenchen

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

end