--- 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)
--- 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 *}