equal
deleted
inserted
replaced
9 |
9 |
10 *** General *** |
10 *** General *** |
11 |
11 |
12 * Document antiquotations @{prf} and @{full_prf} output proof terms |
12 * Document antiquotations @{prf} and @{full_prf} output proof terms |
13 (again) in the same way as commands 'prf' and 'full_prf'. |
13 (again) in the same way as commands 'prf' and 'full_prf'. |
|
14 |
|
15 * Computations generated by the code generator can be embedded |
|
16 directly into ML, alongside with @{code} antiquotations, using |
|
17 the following antiquotations: |
|
18 |
|
19 @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a |
|
20 @{computation_conv … terms: … datatypes: …} : ('ml -> conv) -> Proof.context -> conv |
|
21 @{computation_check terms: … datatypes: …} : Proof.context -> conv |
|
22 |
|
23 See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy |
|
24 and src/HOL/Decision_Procs/Reflective_Field.thy for examples. |
14 |
25 |
15 |
26 |
16 *** Prover IDE -- Isabelle/Scala/jEdit *** |
27 *** Prover IDE -- Isabelle/Scala/jEdit *** |
17 |
28 |
18 * Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT |
29 * Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT |