equal
deleted
inserted
replaced
1320 delegated to an Isar proof, which often involves automated tools. |
1320 delegated to an Isar proof, which often involves automated tools. |
1321 |
1321 |
1322 @{rail \<open> |
1322 @{rail \<open> |
1323 @@{command consider} @{syntax obtain_clauses} |
1323 @@{command consider} @{syntax obtain_clauses} |
1324 ; |
1324 ; |
1325 @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') |
1325 @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \<newline> |
1326 @'where' (@{syntax props} + @'and') |
1326 @'where' concl prems @{syntax for_fixes} |
|
1327 ; |
|
1328 concl: (@{syntax props} + @'and') |
|
1329 ; |
|
1330 prems: (@'if' (@{syntax props'} + @'and'))? |
1327 ; |
1331 ; |
1328 @@{command guess} (@{syntax "fixes"} + @'and') |
1332 @@{command guess} (@{syntax "fixes"} + @'and') |
1329 \<close>} |
1333 \<close>} |
1330 |
1334 |
1331 \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) |
1335 \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) |