--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/Inc/Pcount.thy	Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,20 @@
+(* 
+    File:	 TLA/ex/inc/Pcount.thy
+    Author:      Stephan Merz
+    Copyright:   1997 University of Munich
+
+    Theory Name: Pcount
+    Logic Image: TLA
+
+Data type "program counter" for the increment example.
+Isabelle/HOL's datatype package generates useful simplifications
+and case distinction tactics.
+*)
+
+Pcount  =  HOL + Arith +
+
+datatype pcount = a | b | g
+
+end
+
+ML