src/HOLCF/IOA/NTP/Lemmas.thy
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 12218 6597093b77e7
child 17244 0b2ff9541727
permissions -rw-r--r--
Merged in license change from Isabelle2004
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/IOA/NTP/Lemmas.thy
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     2
    ID:         $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     3
    Author:     Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     4
12218
wenzelm
parents: 10215
diff changeset
     5
Arithmetic lemmas.
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     6
*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     7
10215
1ead773b365e *** empty log message ***
nipkow
parents: 10212
diff changeset
     8
Lemmas = NatArith