# HG changeset patch
# User wenzelm
# Date 1191433773 -7200
# Node ID b7866aea0815bea2407200f54f1a5594efcbd443
# Parent  bfb619994060a8946f8b4c8e393144e69e6891e4
avoid unnamed infixes;

diff -r bfb619994060 -r b7866aea0815 src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Wed Oct 03 19:36:05 2007 +0200
+++ b/src/HOL/Induct/Com.thy	Wed Oct 03 19:49:33 2007 +0200
@@ -11,20 +11,18 @@
 theory Com imports Main begin
 
 typedecl loc
-
 types  state = "loc => nat"
-       n2n2n = "nat => nat => nat"
 
 datatype
   exp = N nat
       | X loc
-      | Op n2n2n exp exp
+      | Op "nat => nat => nat" exp exp
       | valOf com exp          ("VALOF _ RESULTIS _"  60)
 and
   com = SKIP
-      | ":="  loc exp          (infixl  60)
-      | Semi  com com          ("_;;_"  [60, 60] 60)
-      | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
+      | Assign loc exp         (infixl ":=" 60)
+      | Semi com com           ("_;;_"  [60, 60] 60)
+      | Cond exp com com       ("IF _ THEN _ ELSE _"  60)
       | While exp com          ("WHILE _ DO _"  60)
 
 
diff -r bfb619994060 -r b7866aea0815 src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Wed Oct 03 19:36:05 2007 +0200
+++ b/src/HOL/Induct/PropLog.thy	Wed Oct 03 19:49:33 2007 +0200
@@ -21,8 +21,10 @@
 
 subsection {* The datatype of propositions *}
 
-datatype
-    'a pl = false | var 'a ("#_" [1000]) | "->" "'a pl" "'a pl" (infixr 90)
+datatype 'a pl =
+  false |
+  var 'a ("#_" [1000]) |
+  imp "'a pl" "'a pl" (infixr "->" 90)
 
 subsection {* The proof system *}