Changed syntax of inductive.
authorberghofe
Wed Oct 21 17:48:02 1998 +0200 (1998-10-21)
changeset 57170d28dbe484b6
parent 5716 a3d2a6b6693e
child 5718 e5094d678285
Changed syntax of inductive.
src/HOL/Induct/Acc.thy
src/HOL/Induct/Exp.thy
src/HOL/Induct/Term.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/ex/Primrec.thy
     1.1 --- a/src/HOL/Induct/Acc.thy	Wed Oct 21 17:46:00 1998 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Wed Oct 21 17:48:02 1998 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  inductive "acc(r)"
     1.5    intrs
     1.6      pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
     1.7 -  monos     "[Pow_mono]"
     1.8 +  monos     Pow_mono
     1.9  
    1.10  syntax        termi :: "('a * 'a)set => 'a set"
    1.11  translations "termi r" == "acc(r^-1)"
     2.1 --- a/src/HOL/Induct/Exp.thy	Wed Oct 21 17:46:00 1998 +0200
     2.2 +++ b/src/HOL/Induct/Exp.thy	Wed Oct 21 17:48:02 1998 +0200
     2.3 @@ -27,7 +27,7 @@
     2.4      valOf  "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
     2.5              ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
     2.6  
     2.7 -  monos "[exec_mono]"
     2.8 +  monos exec_mono
     2.9  
    2.10  end
    2.11  
     3.1 --- a/src/HOL/Induct/Term.thy	Wed Oct 21 17:46:00 1998 +0200
     3.2 +++ b/src/HOL/Induct/Term.thy	Wed Oct 21 17:48:02 1998 +0200
     3.3 @@ -28,7 +28,7 @@
     3.4  inductive "term(A)"
     3.5    intrs
     3.6      APP_I "[| M: A;  N : list(term(A)) |] ==> Scons M N : term(A)"
     3.7 -  monos   "[list_mono]"
     3.8 +  monos   list_mono
     3.9  
    3.10  defs
    3.11    (*defining abstraction/representation functions for term list...*)
     4.1 --- a/src/HOL/Lambda/InductTermi.thy	Wed Oct 21 17:46:00 1998 +0200
     4.2 +++ b/src/HOL/Lambda/InductTermi.thy	Wed Oct 21 17:48:02 1998 +0200
     4.3 @@ -17,6 +17,6 @@
     4.4  VarI "rs : lists IT ==> (Var n)$$rs : IT"
     4.5  LambdaI "r : IT ==> Abs r : IT"
     4.6  BetaI "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
     4.7 -monos "[lists_mono]"
     4.8 +monos lists_mono
     4.9  
    4.10  end
     5.1 --- a/src/HOL/ex/Primrec.thy	Wed Oct 21 17:46:00 1998 +0200
     5.2 +++ b/src/HOL/ex/Primrec.thy	Wed Oct 21 17:48:02 1998 +0200
     5.3 @@ -67,6 +67,6 @@
     5.4      PROJ     "PROJ i : PRIMREC"
     5.5      COMP     "[| g: PRIMREC; fs: lists PRIMREC |] ==> COMP g fs : PRIMREC"
     5.6      PREC     "[| f: PRIMREC; g: PRIMREC |] ==> PREC f g: PRIMREC"
     5.7 -  monos      "[lists_mono]"
     5.8 +  monos      lists_mono
     5.9  
    5.10  end