src/HOL/Main.thy
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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9619
6125cc9efc18 fixed deps;
wenzelm
parents: 9447
diff changeset
     1
6125cc9efc18 fixed deps;
wenzelm
parents: 9447
diff changeset
     2
(*theory Main includes everything; note that theory
6125cc9efc18 fixed deps;
wenzelm
parents: 9447
diff changeset
     3
  PreList already includes most HOL theories*)
6125cc9efc18 fixed deps;
wenzelm
parents: 9447
diff changeset
     4
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
     5
theory Main = Map + String:
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
     6
10261
bb2f1e859177 tuned declarations;
wenzelm
parents: 9876
diff changeset
     7
(*belongs to theory List*)
bb2f1e859177 tuned declarations;
wenzelm
parents: 9876
diff changeset
     8
declare lists_mono [mono]
bb2f1e859177 tuned declarations;
wenzelm
parents: 9876
diff changeset
     9
declare map_cong [recdef_cong]
10386
581a5a143994 provide case names for rev_induct, rev_cases;
wenzelm
parents: 10261
diff changeset
    10
lemmas rev_induct [case_names Nil snoc] = rev_induct
581a5a143994 provide case names for rev_induct, rev_cases;
wenzelm
parents: 10261
diff changeset
    11
  and rev_cases [case_names Nil snoc] = rev_exhaust
9768
a589b1d75b7b lemmas [mono] = lists_mono;
wenzelm
parents: 9650
diff changeset
    12
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    13
end