Slides/ROOT2.ML
author Christian Urban <urbanc@in.tum.de>
Mon, 17 Jan 2011 12:33:37 +0000
changeset 2662 7c5bca978886
parent 2485 6bab47906dbe
child 2748 6f38e357b337
permissions -rw-r--r--
eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2485
6bab47906dbe added example about datatypes
Christian Urban <urbanc@in.tum.de>
parents: 2351
diff changeset
     1
(* show_question_marks := false; *)
6bab47906dbe added example about datatypes
Christian Urban <urbanc@in.tum.de>
parents: 2351
diff changeset
     2
2351
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
quick_and_dirty := true;
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
2485
6bab47906dbe added example about datatypes
Christian Urban <urbanc@in.tum.de>
parents: 2351
diff changeset
     5
2351
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
no_document use_thy "LaTeXsugar";
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
use_thy "Slides2"