blob: 6be971e2991760859082f920b6b1f0bfaf1f3f39 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
(* Some checks for X-Symbol behaviour.
$Id$
*)
theory XSymbolTests = Main:
(* 28.8.02: bug in pg-remove-specials broke this; now fixed *)
lemma "A ==> A" . -- OK
consts A :: bool
lemma "A ==> A" . -- "xsymbols not displayed?"
(* Test electric token input: writing a token
like \ <alpha> (without space, \<alpha>) should immediately
replace it. *)
constdefs
P1 :: bool ("P\<^sub>1") (* subscript *)
"P\<^sub>1 == True"
P2 :: bool ("P\<^sup>2") (* superscript *)
"P\<^sup>2 == True"
(* Buglet here: if we enable x-sym during scripting,
goals/response flks are not updated, so xsyms
do not appear in output windows. Stoping/starting
prover fixes.
*)
theorem "P\<^sub>1 \<and> P\<^sup>2"; (* check fonts in goals window *)
by (simp add: P1_def P2_def) (* .. and response window *)
(* BUG: \<and> not appearing in response *)
consts
"P\<^sup>\<alpha>" :: bool (* superscript of a token char *)
"\<^bold>X" :: bool (* bold character *)
(* Markus reports that \<cdot> is saved in the file as
an 8-bit character. I can't repeat that with XEmacs 21.4,
unless I set the relevant X-Symbol menu option. *)
(*
Another X-Symbol oddity: sometimes the _first_ buffer to
be visited displays _some_ characters as \2xx, e.g.
for \<circ>. But subsequent buffers to be visited work
fine. Problem is stable for turning x-symbol on/off.
Revisting the first buffer cures the problem.
I can't easily repeat the problem...
*)
consts
iter :: "('a => 'a) => nat => ('a => 'a)"
primrec
"iter f 0 = id"
"iter f (Suc n) = f \<circ> (iter f n)"
end
|
