Quotes now optional around inductive set

--- a/src/HOL/IMP/Expr.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/IMP/Expr.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -28,7 +28,7 @@
        "-a->"    :: "[aexp*state,nat] => bool"         (infixl 50)
 translations
     "aesig -a-> n" == "(aesig,n) : evala"
-inductive "evala"
+inductive evala
   intrs 
     N   "(N(n),s) -a-> n"
     X   "(X(x),s) -a-> s(x)"
@@ -55,7 +55,7 @@
 translations
     "besig -b-> b" == "(besig,b) : evalb"
 
-inductive "evalb"
+inductive evalb
  intrs (*avoid clash with ML constructors true, false*)
     tru   "(true,s) -b-> True"
     fls   "(false,s) -b-> False"

--- a/src/HOL/IMP/Hoare.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/IMP/Hoare.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -17,7 +17,7 @@
 syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
 translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
 
-inductive "hoare"
+inductive hoare
 intrs
   skip "|- {P}SKIP{P}"
   ass  "|- {%s.P(s[a s/x])} x:=a {P}"

--- a/src/HOL/IMP/Natural.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/IMP/Natural.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -18,7 +18,7 @@
   "s[m/x] ==  (%y. if y=x then m else s y)"
 
 
-inductive "evalc"
+inductive evalc
   intrs
     Skip    "<SKIP,s> -c-> s"
 

--- a/src/HOL/IMP/Transition.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/IMP/Transition.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -25,7 +25,7 @@
 	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
 
 
-inductive "evalc1"
+inductive evalc1
   intrs
     Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
 

--- a/src/HOL/Lambda/Eta.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/Lambda/Eta.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -27,7 +27,7 @@
 defs
   decr_def "decr t i == t[Var i/i]"
 
-inductive "eta"
+inductive eta
 intrs
    eta  "~free s 0 ==> Fun(s @ Var 0) -e> decr s 0"
    appL  "s -e> t ==> s@u -e> t@u"

--- a/src/HOL/Lambda/Lambda.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -48,7 +48,7 @@
   "s -> t"  == "(s,t) : beta"
   "s ->> t" == "(s,t) : beta^*"
 
-inductive "beta"
+inductive beta
 intrs
    beta  "(Fun s) @ t -> s[t/0]"
    appL  "s -> t ==> s@u -> t@u"

--- a/src/HOL/Lambda/ParRed.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -15,7 +15,7 @@
 translations
   "s => t" == "(s,t) : par_beta"
 
-inductive "par_beta"
+inductive par_beta
   intrs
     var   "Var n => Var n"
     abs   "s => t ==> Fun s => Fun t"

--- a/src/HOL/ex/Comb.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/ex/Comb.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -32,7 +32,7 @@
   "x -1-> y" == "(x,y) : contract"
   "x ---> y" == "(x,y) : contract^*"
 
-inductive "contract"
+inductive contract
   intrs
     K     "K#x#y -1-> x"
     S     "S#x#y#z -1-> (x#z)#(y#z)"
@@ -52,7 +52,7 @@
   "x =1=> y" == "(x,y) : parcontract"
   "x ===> y" == "(x,y) : parcontract^*"
 
-inductive "parcontract"
+inductive parcontract
   intrs
     refl  "x =1=> x"
     K     "K#x#y =1=> x"

--- a/src/HOL/ex/Mutil.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/ex/Mutil.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -15,7 +15,7 @@
   below   :: nat => nat set
   evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
 
-inductive "domino"
+inductive domino
   intrs
     horiz  "{(i, j), (i, Suc j)} : domino"
     vertl  "{(i, j), (Suc i, j)} : domino"

--- a/src/HOL/ex/Perm.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/ex/Perm.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -14,7 +14,7 @@
 translations
     "x <~~> y" == "(x,y) : perm"
 
-inductive "perm"
+inductive perm
   intrs
     Nil   "[] <~~> []"
     swap  "y#x#l <~~> x#y#l"