Quotes now optional around inductive set
authorpaulson
Thu Jun 06 14:39:44 1996 +0200 (1996-06-06)
changeset 1789aade046ec6d5
parent 1788 ca62fab4ce92
child 1790 2f3694c50101
Quotes now optional around inductive set
src/HOL/IMP/Expr.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Natural.thy
src/HOL/IMP/Transition.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ParRed.thy
src/HOL/ex/Comb.thy
src/HOL/ex/Mutil.thy
src/HOL/ex/Perm.thy
     1.1 --- a/src/HOL/IMP/Expr.thy	Thu Jun 06 13:13:18 1996 +0200
     1.2 +++ b/src/HOL/IMP/Expr.thy	Thu Jun 06 14:39:44 1996 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4         "-a->"    :: "[aexp*state,nat] => bool"         (infixl 50)
     1.5  translations
     1.6      "aesig -a-> n" == "(aesig,n) : evala"
     1.7 -inductive "evala"
     1.8 +inductive evala
     1.9    intrs 
    1.10      N   "(N(n),s) -a-> n"
    1.11      X   "(X(x),s) -a-> s(x)"
    1.12 @@ -55,7 +55,7 @@
    1.13  translations
    1.14      "besig -b-> b" == "(besig,b) : evalb"
    1.15  
    1.16 -inductive "evalb"
    1.17 +inductive evalb
    1.18   intrs (*avoid clash with ML constructors true, false*)
    1.19      tru   "(true,s) -b-> True"
    1.20      fls   "(false,s) -b-> False"
     2.1 --- a/src/HOL/IMP/Hoare.thy	Thu Jun 06 13:13:18 1996 +0200
     2.2 +++ b/src/HOL/IMP/Hoare.thy	Thu Jun 06 14:39:44 1996 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
     2.5  translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
     2.6  
     2.7 -inductive "hoare"
     2.8 +inductive hoare
     2.9  intrs
    2.10    skip "|- {P}SKIP{P}"
    2.11    ass  "|- {%s.P(s[a s/x])} x:=a {P}"
     3.1 --- a/src/HOL/IMP/Natural.thy	Thu Jun 06 13:13:18 1996 +0200
     3.2 +++ b/src/HOL/IMP/Natural.thy	Thu Jun 06 14:39:44 1996 +0200
     3.3 @@ -18,7 +18,7 @@
     3.4    "s[m/x] ==  (%y. if y=x then m else s y)"
     3.5  
     3.6  
     3.7 -inductive "evalc"
     3.8 +inductive evalc
     3.9    intrs
    3.10      Skip    "<SKIP,s> -c-> s"
    3.11  
     4.1 --- a/src/HOL/IMP/Transition.thy	Thu Jun 06 13:13:18 1996 +0200
     4.2 +++ b/src/HOL/IMP/Transition.thy	Thu Jun 06 14:39:44 1996 +0200
     4.3 @@ -25,7 +25,7 @@
     4.4  	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
     4.5  
     4.6  
     4.7 -inductive "evalc1"
     4.8 +inductive evalc1
     4.9    intrs
    4.10      Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
    4.11  
     5.1 --- a/src/HOL/Lambda/Eta.thy	Thu Jun 06 13:13:18 1996 +0200
     5.2 +++ b/src/HOL/Lambda/Eta.thy	Thu Jun 06 14:39:44 1996 +0200
     5.3 @@ -27,7 +27,7 @@
     5.4  defs
     5.5    decr_def "decr t i == t[Var i/i]"
     5.6  
     5.7 -inductive "eta"
     5.8 +inductive eta
     5.9  intrs
    5.10     eta  "~free s 0 ==> Fun(s @ Var 0) -e> decr s 0"
    5.11     appL  "s -e> t ==> s@u -e> t@u"
     6.1 --- a/src/HOL/Lambda/Lambda.thy	Thu Jun 06 13:13:18 1996 +0200
     6.2 +++ b/src/HOL/Lambda/Lambda.thy	Thu Jun 06 14:39:44 1996 +0200
     6.3 @@ -48,7 +48,7 @@
     6.4    "s -> t"  == "(s,t) : beta"
     6.5    "s ->> t" == "(s,t) : beta^*"
     6.6  
     6.7 -inductive "beta"
     6.8 +inductive beta
     6.9  intrs
    6.10     beta  "(Fun s) @ t -> s[t/0]"
    6.11     appL  "s -> t ==> s@u -> t@u"
     7.1 --- a/src/HOL/Lambda/ParRed.thy	Thu Jun 06 13:13:18 1996 +0200
     7.2 +++ b/src/HOL/Lambda/ParRed.thy	Thu Jun 06 14:39:44 1996 +0200
     7.3 @@ -15,7 +15,7 @@
     7.4  translations
     7.5    "s => t" == "(s,t) : par_beta"
     7.6  
     7.7 -inductive "par_beta"
     7.8 +inductive par_beta
     7.9    intrs
    7.10      var   "Var n => Var n"
    7.11      abs   "s => t ==> Fun s => Fun t"
     8.1 --- a/src/HOL/ex/Comb.thy	Thu Jun 06 13:13:18 1996 +0200
     8.2 +++ b/src/HOL/ex/Comb.thy	Thu Jun 06 14:39:44 1996 +0200
     8.3 @@ -32,7 +32,7 @@
     8.4    "x -1-> y" == "(x,y) : contract"
     8.5    "x ---> y" == "(x,y) : contract^*"
     8.6  
     8.7 -inductive "contract"
     8.8 +inductive contract
     8.9    intrs
    8.10      K     "K#x#y -1-> x"
    8.11      S     "S#x#y#z -1-> (x#z)#(y#z)"
    8.12 @@ -52,7 +52,7 @@
    8.13    "x =1=> y" == "(x,y) : parcontract"
    8.14    "x ===> y" == "(x,y) : parcontract^*"
    8.15  
    8.16 -inductive "parcontract"
    8.17 +inductive parcontract
    8.18    intrs
    8.19      refl  "x =1=> x"
    8.20      K     "K#x#y =1=> x"
     9.1 --- a/src/HOL/ex/Mutil.thy	Thu Jun 06 13:13:18 1996 +0200
     9.2 +++ b/src/HOL/ex/Mutil.thy	Thu Jun 06 14:39:44 1996 +0200
     9.3 @@ -15,7 +15,7 @@
     9.4    below   :: nat => nat set
     9.5    evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
     9.6  
     9.7 -inductive "domino"
     9.8 +inductive domino
     9.9    intrs
    9.10      horiz  "{(i, j), (i, Suc j)} : domino"
    9.11      vertl  "{(i, j), (Suc i, j)} : domino"
    10.1 --- a/src/HOL/ex/Perm.thy	Thu Jun 06 13:13:18 1996 +0200
    10.2 +++ b/src/HOL/ex/Perm.thy	Thu Jun 06 14:39:44 1996 +0200
    10.3 @@ -14,7 +14,7 @@
    10.4  translations
    10.5      "x <~~> y" == "(x,y) : perm"
    10.6  
    10.7 -inductive "perm"
    10.8 +inductive perm
    10.9    intrs
   10.10      Nil   "[] <~~> []"
   10.11      swap  "y#x#l <~~> x#y#l"