63 Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*) |
63 Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*) |
64 Try :: "['a => 'a, 'a] => 'a" |
64 Try :: "['a => 'a, 'a] => 'a" |
65 Repeat :: "['a => 'a, 'a] => 'a" |
65 Repeat :: "['a => 'a, 'a] => 'a" |
66 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10) |
66 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10) |
67 While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9) |
67 While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9) |
|
68 (*WN100723 because of "Error in syntax translation" below... |
68 (*'b => bool doesn't work with "contains_root _"*) |
69 (*'b => bool doesn't work with "contains_root _"*) |
69 Letpar :: "['a, 'a => 'b] => 'b" |
70 Letpar :: "['a, 'a => 'b] => 'b" |
70 (*--- defined in Isabelle/scr/HOL/HOL.thy: |
71 (*--- defined in Isabelle/scr/HOL/HOL.thy: |
71 Let :: "['a, 'a => 'b] => 'b" |
72 Let :: "['a, 'a => 'b] => 'b" |
72 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
73 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
73 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
74 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
74 %x. P x .. lambda is defined in Isabelles meta logic |
75 %x. P x .. lambda is defined in Isabelles meta logic |
75 --- *) |
76 --- *) |
76 |
77 *) |
77 |
|
78 failtac :: 'a |
78 failtac :: 'a |
79 idletac :: 'a |
79 idletac :: 'a |
80 (*... + RECORD IN 'screxpr' in Script.ML *) |
80 (*... + RECORD IN 'screxpr' in Script.ML *) |
81 |
81 |
82 (*for scripts generated automatically from rls*) |
82 (*for scripts generated automatically from rls*) |
131 ("((Script Testchk (_ _ =))// |
131 ("((Script Testchk (_ _ =))// |
132 (_))" 9) |
132 (_))" 9) |
133 (*... + RECORD IN 'subpbls' in Script.ML *) |
133 (*... + RECORD IN 'subpbls' in Script.ML *) |
134 (*SHIFT -> resp.thys ----^^^----------------------------*) |
134 (*SHIFT -> resp.thys ----^^^----------------------------*) |
135 |
135 |
|
136 (*Makarius 10.03 |
136 syntax |
137 syntax |
137 |
138 |
138 "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10) |
139 "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10) |
139 |
140 |
140 translations |
141 translations |
141 |
142 |
142 "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)" |
143 "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)" |
143 "letpar x = a in e" == "Letpar a (%x. e)" |
144 "letpar x = a in e" == "Letpar a (%x. e)" |
|
145 *** Error in syntax translation rule: rhs contains extra variables |
|
146 *** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e)) |
|
147 *** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script.thy"). |
|
148 *) |
|
149 |
|
150 ML{* (*the former Script.ML*) |
|
151 |
|
152 *} |
144 |
153 |
145 end |
154 end |