Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
authormueller
Wed, 31 May 1995 10:46:46 +0200
changeset 1139 993e475e70e2
parent 1138 82fd99d5a6ff
child 1140 0a804a71274a
*** empty log message ***
src/HOL/IOA/ABP/Env.thy file | annotate | diff | comparison | revisions
src/HOL/IOA/ABP/Impl.thy file | annotate | diff | comparison | revisions
src/HOL/IOA/ABP/Impl_finite.thy file | annotate | diff | comparison | revisions
src/HOL/IOA/ABP/Lemmas.ML file | annotate | diff | comparison | revisions
src/HOL/IOA/ABP/Lemmas.thy file | annotate | diff | comparison | revisions
src/HOL/IOA/ABP/Packet.thy file | annotate | diff | comparison | revisions
src/HOL/IOA/ABP/Receiver.thy file | annotate | diff | comparison | revisions
src/HOL/IOA/ABP/Sender.thy file | annotate | diff | comparison | revisions
src/HOL/IOA/ABP/Spec.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/IOA/ABP/Env.thy	Wed May 31 10:45:00 1995 +0200
+++ b/src/HOL/IOA/ABP/Env.thy	Wed May 31 10:46:46 1995 +0200
@@ -1,4 +1,5 @@
-(*  Title:      HOL/IOA/ABP/Impl.thy
+(*  Title:      HOL/IOA/example/Impl.thy
+by (Action.action.induct_tac "a" 1);
     ID:         $Id$
     Author:     Tobias Nipkow & Konrad Slind
     Copyright   1994  TU Muenchen
--- a/src/HOL/IOA/ABP/Impl.thy	Wed May 31 10:45:00 1995 +0200
+++ b/src/HOL/IOA/ABP/Impl.thy	Wed May 31 10:46:46 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Impl.thy
+(*  Title:      HOL/IOA/example/Impl.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
 The implementation
 *)
--- a/src/HOL/IOA/ABP/Impl_finite.thy	Wed May 31 10:45:00 1995 +0200
+++ b/src/HOL/IOA/ABP/Impl_finite.thy	Wed May 31 10:46:46 1995 +0200
@@ -1,9 +1,9 @@
-(*  Title:      HOL/IOA/ABP/Impl_finite.thy
+(*  Title:      HOL/IOA/example/Impl.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
-The finite implementation
+The implementation
 *)
 
 Impl_finite = Sender + Receiver +  Abschannel_finite +
--- a/src/HOL/IOA/ABP/Lemmas.ML	Wed May 31 10:45:00 1995 +0200
+++ b/src/HOL/IOA/ABP/Lemmas.ML	Wed May 31 10:46:46 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Lemmas.ML
+(*  Title:      HOL/IOA/example/Lemmas.ML
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
 *)
 
--- a/src/HOL/IOA/ABP/Lemmas.thy	Wed May 31 10:45:00 1995 +0200
+++ b/src/HOL/IOA/ABP/Lemmas.thy	Wed May 31 10:46:46 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Lemmas.thy
+(*  Title:      HOL/IOA/example/Lemmas.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
 Arithmetic lemmas
 *)
--- a/src/HOL/IOA/ABP/Packet.thy	Wed May 31 10:45:00 1995 +0200
+++ b/src/HOL/IOA/ABP/Packet.thy	Wed May 31 10:46:46 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Packet.thy
+(*  Title:      HOL/IOA/example/Packet.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
 Packets
 *)
--- a/src/HOL/IOA/ABP/Receiver.thy	Wed May 31 10:45:00 1995 +0200
+++ b/src/HOL/IOA/ABP/Receiver.thy	Wed May 31 10:46:46 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Receiver.thy
+(*  Title:      HOL/IOA/example/Receiver.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
 The implementation: receiver
 *)
--- a/src/HOL/IOA/ABP/Sender.thy	Wed May 31 10:45:00 1995 +0200
+++ b/src/HOL/IOA/ABP/Sender.thy	Wed May 31 10:46:46 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Sender.thy
+(*  Title:      HOL/IOA/example/Sender.thy
     ID:         $Id$
     Author:     Tobias Nipkow & Konrad Slind
-    Copyright   1995  TU Muenchen
+    Copyright   1994  TU Muenchen
 
 The implementation: sender
 *)
--- a/src/HOL/IOA/ABP/Spec.thy	Wed May 31 10:45:00 1995 +0200
+++ b/src/HOL/IOA/ABP/Spec.thy	Wed May 31 10:46:46 1995 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IOA/ABP/Spec.thy
+(*  Title:      HOL/IOA/example/Spec.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Olaf Mueller
-    Copyright   1995  TU Muenchen
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
 
 The specification of reliable transmission
 *)
isabelle