src/HOL/Induct/Exp.ML
 changeset 5148 74919e8f221c parent 5143 b94cd208f073 child 5223 4cb05273f764
equal inserted replaced
5147:825877190618 5148:74919e8f221c
`    65   using eval restricted to its functional part.  Note that the execution`
`    65   using eval restricted to its functional part.  Note that the execution`
`    66   (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that `
`    66   (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that `
`    67   the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is`
`    67   the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is`
`    68   functional on the argument (c,s).`
`    68   functional on the argument (c,s).`
`    69 *)`
`    69 *)`
`    70 Goal`
`    70 Goal "(c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \`
`    71     "!!x. (c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \`
`    71 \     ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";`
`    72 \         ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";`
`       `
`    73 by (etac exec.induct 1);`
`    72 by (etac exec.induct 1);`
`    74 by (ALLGOALS Full_simp_tac);`
`    73 by (ALLGOALS Full_simp_tac);`
`    75 by (Blast_tac 3);`
`    74 by (Blast_tac 3);`
`    76 by (Blast_tac 1);`
`    75 by (Blast_tac 1);`
`    77 by (rewtac Unique_def);`
`    76 by (rewtac Unique_def);`