src/HOL/MicroJava/J/WellType.thy
changeset 23757 087b0a241557
parent 22271 51a80e238b29
child 35102 cc7a0b9f938c
     1.1 --- a/src/HOL/MicroJava/J/WellType.thy	Wed Jul 11 11:29:44 2007 +0200
     1.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Wed Jul 11 11:32:02 2007 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4  -- "method body with parameter names, local variables, block, result expression."
     1.5  -- "local variables might include This, which is hidden anyway"
     1.6    
     1.7 -inductive2
     1.8 +inductive
     1.9    ty_expr :: "'c env => expr => ty => bool" ("_ \<turnstile> _ :: _" [51, 51, 51] 50)
    1.10    and ty_exprs :: "'c env => expr list => ty list => bool" ("_ \<turnstile> _ [::] _" [51, 51, 51] 50)
    1.11    and wt_stmt :: "'c env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51, 51] 50)