changeset 6301 | 08245f5a436d |
parent 6255 | db63752140c7 |
child 7881 | 1b1db39a110b |
6300:3815b5b095cb | 6301:08245f5a436d |
---|---|
251 |
251 |
252 (* Example: |
252 (* Example: |
253 |
253 |
254 val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))"; |
254 val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))"; |
255 by (enabled_tac prem 1); |
255 by (enabled_tac prem 1); |
256 auto(); |
256 by Auto_tac; |
257 |
257 |
258 *) |
258 *) |