| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Sat, 19 Mar 2016 21:06:48 +0000 | |
| branch | Nominal2-Isabelle2016 |
| changeset 3243 | c4f31f1564b7 |
| parent 2871 | b58073719b06 |
| permissions | -rw-r--r-- |
|
2871
b58073719b06
Update Quotient/TODO and remove some attic code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
948
diff
changeset
|
1 |
(* Could go in the programming tutorial *) |
|
379
57bde65f6eb2
Removed unused things from QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
|
|
2871
b58073719b06
Update Quotient/TODO and remove some attic code
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
948
diff
changeset
|
3 |
ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
|