6 theory Overview |
6 theory Overview |
7 imports Imperative_HOL "~~/src/HOL/Library/LaTeXsugar" |
7 imports Imperative_HOL "~~/src/HOL/Library/LaTeXsugar" |
8 begin |
8 begin |
9 |
9 |
10 (* type constraints with spacing *) |
10 (* type constraints with spacing *) |
11 setup {* |
11 no_syntax (output) |
12 let |
12 "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3) |
13 val typ = Simple_Syntax.read_typ; |
13 "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3) |
14 in |
14 |
15 Sign.del_syntax (Symbol.xsymbolsN, false) |
15 syntax (output) |
16 [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
16 "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) |
17 ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #> |
17 "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3) |
18 Sign.add_syntax (Symbol.xsymbolsN, false) |
18 (*>*) |
19 [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)), |
|
20 ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))] |
|
21 end |
|
22 *}(*>*) |
|
23 |
19 |
24 text {* |
20 text {* |
25 @{text "Imperative HOL"} is a leightweight framework for reasoning |
21 @{text "Imperative HOL"} is a leightweight framework for reasoning |
26 about imperative data structures in @{text "Isabelle/HOL"} |
22 about imperative data structures in @{text "Isabelle/HOL"} |
27 @{cite "Nipkow-et-al:2002:tutorial"}. Its basic ideas are described in |
23 @{cite "Nipkow-et-al:2002:tutorial"}. Its basic ideas are described in |