Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Main.thy
author wenzelm
Fri, 10 Nov 2000 19:03:55 +0100
changeset 10434 6ea4735c3955
parent 10386 581a5a143994
child 10519 ade64af4c57c
permissions -rw-r--r--
simplified atomize; added inductive_rulify2 (to accomodate malformed induction rules);
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















isabelle