For the Isar version of the ZF logics manual
authorpaulson
Tue Aug 19 13:53:58 2003 +0200 (2003-08-19)
changeset 1415212f6f18e7afc
parent 14151 b8bb6a6a2c46
child 14153 76a6ba67bd15
For the Isar version of the ZF logics manual
doc-src/ZF/FOL-eg.txt
doc-src/ZF/FOL_examples.thy
doc-src/ZF/IFOL_examples.thy
doc-src/ZF/IsaMakefile
doc-src/ZF/ROOT.ML
doc-src/ZF/ZF-eg.txt
doc-src/ZF/ZF_examples.thy
doc-src/ZF/isabelle.sty
doc-src/ZF/isabellesym.sty
     1.1 --- a/doc-src/ZF/FOL-eg.txt	Fri Aug 15 13:45:39 2003 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,245 +0,0 @@
     1.4 -(**** FOL examples ****)
     1.5 -
     1.6 -Pretty.setmargin 72;  (*existing macros just allow this margin*)
     1.7 -print_depth 0;
     1.8 -
     1.9 -(*** Intuitionistic examples ***)
    1.10 -
    1.11 -context IFOL.thy;
    1.12 -
    1.13 -(*Quantifier example from Logic&Computation*)
    1.14 -Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
    1.15 -by (resolve_tac [impI] 1);
    1.16 -by (resolve_tac [allI] 1);
    1.17 -by (resolve_tac [exI] 1);
    1.18 -by (eresolve_tac [exE] 1);
    1.19 -choplev 2;
    1.20 -by (eresolve_tac [exE] 1);
    1.21 -by (resolve_tac [exI] 1);
    1.22 -by (eresolve_tac [allE] 1);
    1.23 -by (assume_tac 1);
    1.24 -
    1.25 -
    1.26 -(*Example of Dyckhoff's method*)
    1.27 -Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
    1.28 -by (resolve_tac [impI] 1);
    1.29 -by (eresolve_tac [disj_impE] 1);
    1.30 -by (eresolve_tac [imp_impE] 1);
    1.31 -by (eresolve_tac [imp_impE] 1);
    1.32 -by (REPEAT (eresolve_tac [FalseE] 2));
    1.33 -by (assume_tac 1);
    1.34 -
    1.35 -
    1.36 -
    1.37 -
    1.38 -
    1.39 -(*** Classical examples ***)
    1.40 -
    1.41 -context FOL.thy;
    1.42 -
    1.43 -Goal "EX y. ALL x. P(y)-->P(x)";
    1.44 -by (resolve_tac [exCI] 1);
    1.45 -by (resolve_tac [allI] 1);
    1.46 -by (resolve_tac [impI] 1);
    1.47 -by (eresolve_tac [allE] 1);
    1.48 -prth (allI RSN (2,swap));
    1.49 -by (eresolve_tac [it] 1);
    1.50 -by (resolve_tac [impI] 1);
    1.51 -by (eresolve_tac [notE] 1);
    1.52 -by (assume_tac 1);
    1.53 -Goal "EX y. ALL x. P(y)-->P(x)";
    1.54 -by (Blast_tac 1);
    1.55 -
    1.56 -
    1.57 -
    1.58 -- Goal "EX y. ALL x. P(y)-->P(x)";
    1.59 -Level 0
    1.60 -EX y. ALL x. P(y) --> P(x)
    1.61 - 1. EX y. ALL x. P(y) --> P(x)
    1.62 -- by (resolve_tac [exCI] 1);
    1.63 -Level 1
    1.64 -EX y. ALL x. P(y) --> P(x)
    1.65 - 1. ALL y. ~(ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)
    1.66 -- by (resolve_tac [allI] 1);
    1.67 -Level 2
    1.68 -EX y. ALL x. P(y) --> P(x)
    1.69 - 1. !!x. ALL y. ~(ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)
    1.70 -- by (resolve_tac [impI] 1);
    1.71 -Level 3
    1.72 -EX y. ALL x. P(y) --> P(x)
    1.73 - 1. !!x. [| ALL y. ~(ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)
    1.74 -- by (eresolve_tac [allE] 1);
    1.75 -Level 4
    1.76 -EX y. ALL x. P(y) --> P(x)
    1.77 - 1. !!x. [| P(?a); ~(ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)
    1.78 -- prth (allI RSN (2,swap));
    1.79 -[| ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) |] ==> ?Q
    1.80 -- by (eresolve_tac [it] 1);
    1.81 -Level 5
    1.82 -EX y. ALL x. P(y) --> P(x)
    1.83 - 1. !!x xa. [| P(?a); ~P(x) |] ==> P(?y3(x)) --> P(xa)
    1.84 -- by (resolve_tac [impI] 1);
    1.85 -Level 6
    1.86 -EX y. ALL x. P(y) --> P(x)
    1.87 - 1. !!x xa. [| P(?a); ~P(x); P(?y3(x)) |] ==> P(xa)
    1.88 -- by (eresolve_tac [notE] 1);
    1.89 -Level 7
    1.90 -EX y. ALL x. P(y) --> P(x)
    1.91 - 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)
    1.92 -- by (assume_tac 1);
    1.93 -Level 8
    1.94 -EX y. ALL x. P(y) --> P(x)
    1.95 -No subgoals!
    1.96 -- Goal "EX y. ALL x. P(y)-->P(x)";
    1.97 -Level 0
    1.98 -EX y. ALL x. P(y) --> P(x)
    1.99 - 1. EX y. ALL x. P(y) --> P(x)
   1.100 -- by (best_tac FOL_dup_cs 1);
   1.101 -Level 1
   1.102 -EX y. ALL x. P(y) --> P(x)
   1.103 -No subgoals!
   1.104 -
   1.105 -
   1.106 -(**** finally, the example FOL/ex/if.ML ****)
   1.107 -
   1.108 -> val prems = goalw if_thy [if_def]
   1.109 -#    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
   1.110 -Level 0
   1.111 -if(P,Q,R)
   1.112 - 1. P & Q | ~P & R
   1.113 -> by (Classical.fast_tac (FOL_cs addIs prems) 1);
   1.114 -Level 1
   1.115 -if(P,Q,R)
   1.116 -No subgoals!
   1.117 -> val ifI = result();
   1.118 -
   1.119 -
   1.120 -> val major::prems = goalw if_thy [if_def]
   1.121 -#    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
   1.122 -Level 0
   1.123 -S
   1.124 - 1. S
   1.125 -> by (cut_facts_tac [major] 1);
   1.126 -Level 1
   1.127 -S
   1.128 - 1. P & Q | ~P & R ==> S
   1.129 -> by (Classical.fast_tac (FOL_cs addIs prems) 1);
   1.130 -Level 2
   1.131 -S
   1.132 -No subgoals!
   1.133 -> val ifE = result();
   1.134 -
   1.135 -> goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
   1.136 -Level 0
   1.137 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.138 - 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.139 -> by (resolve_tac [iffI] 1);
   1.140 -Level 1
   1.141 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.142 - 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))
   1.143 - 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.144 -> by (eresolve_tac [ifE] 1);
   1.145 -Level 2
   1.146 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.147 - 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.148 - 2. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.149 - 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.150 -> by (eresolve_tac [ifE] 1);
   1.151 -Level 3
   1.152 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.153 - 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.154 - 2. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.155 - 3. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.156 - 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.157 -> by (resolve_tac [ifI] 1);
   1.158 -Level 4
   1.159 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.160 - 1. [| P; Q; A; Q |] ==> if(P,A,C)
   1.161 - 2. [| P; Q; A; ~Q |] ==> if(P,B,D)
   1.162 - 3. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.163 - 4. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.164 - 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.165 -> by (resolve_tac [ifI] 1);
   1.166 -Level 5
   1.167 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.168 - 1. [| P; Q; A; Q; P |] ==> A
   1.169 - 2. [| P; Q; A; Q; ~P |] ==> C
   1.170 - 3. [| P; Q; A; ~Q |] ==> if(P,B,D)
   1.171 - 4. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.172 - 5. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
   1.173 - 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
   1.174 -
   1.175 -> choplev 0;
   1.176 -Level 0
   1.177 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.178 - 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.179 -> val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
   1.180 -> by (Classical.fast_tac if_cs 1);
   1.181 -Level 1
   1.182 -if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
   1.183 -No subgoals!
   1.184 -> val if_commute = result();
   1.185 -
   1.186 -> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
   1.187 -Level 0
   1.188 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.189 - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.190 -> by (Classical.fast_tac if_cs 1);
   1.191 -Level 1
   1.192 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.193 -No subgoals!
   1.194 -> val nested_ifs = result();
   1.195 -
   1.196 -
   1.197 -> choplev 0;
   1.198 -Level 0
   1.199 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.200 - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.201 -> by (rewrite_goals_tac [if_def]);
   1.202 -Level 1
   1.203 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.204 - 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
   1.205 -    P & (Q & A | ~Q & B) | ~P & (R & A | ~R & B)
   1.206 -> by (Classical.fast_tac FOL_cs 1);
   1.207 -Level 2
   1.208 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
   1.209 -No subgoals!
   1.210 -
   1.211 -
   1.212 -> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
   1.213 -Level 0
   1.214 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.215 - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.216 -> by (REPEAT (Classical.step_tac if_cs 1));
   1.217 -Level 1
   1.218 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.219 - 1. [| A; ~P; R; ~P; R |] ==> B
   1.220 - 2. [| B; ~P; ~R; ~P; ~R |] ==> A
   1.221 - 3. [| ~P; R; B; ~P; R |] ==> A
   1.222 - 4. [| ~P; ~R; A; ~B; ~P |] ==> R
   1.223 -
   1.224 -> choplev 0;
   1.225 -Level 0
   1.226 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.227 - 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.228 -> by (rewrite_goals_tac [if_def]);
   1.229 -Level 1
   1.230 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.231 - 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
   1.232 -    P & (Q & A | ~Q & B) | ~P & (R & B | ~R & A)
   1.233 -> by (Classical.fast_tac FOL_cs 1);
   1.234 -by: tactic failed
   1.235 -Exception- ERROR raised
   1.236 -Exception failure raised
   1.237 -
   1.238 -> by (REPEAT (Classical.step_tac FOL_cs 1));
   1.239 -Level 2
   1.240 -if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
   1.241 - 1. [| A; ~P; R; ~P; R; ~False |] ==> B
   1.242 - 2. [| A; ~P; R; R; ~False; ~B; ~B |] ==> Q
   1.243 - 3. [| B; ~P; ~R; ~P; ~A |] ==> R
   1.244 - 4. [| B; ~P; ~R; ~Q; ~A |] ==> R
   1.245 - 5. [| B; ~R; ~P; ~A; ~R; Q; ~False |] ==> A
   1.246 - 6. [| ~P; R; B; ~P; R; ~False |] ==> A
   1.247 - 7. [| ~P; ~R; A; ~B; ~R |] ==> P
   1.248 - 8. [| ~P; ~R; A; ~B; ~R |] ==> Q
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/ZF/FOL_examples.thy	Tue Aug 19 13:53:58 2003 +0200
     2.3 @@ -0,0 +1,34 @@
     2.4 +header{*Examples of Classical Reasoning*}
     2.5 +
     2.6 +theory FOL_examples = FOL:
     2.7 +
     2.8 +lemma "EX y. ALL x. P(y)-->P(x)"
     2.9 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    2.10 +apply (rule exCI)
    2.11 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    2.12 +apply (rule allI)
    2.13 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    2.14 +apply (rule impI)
    2.15 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    2.16 +apply (erule allE)
    2.17 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    2.18 +txt{*see below for @{text allI} combined with @{text swap}*}
    2.19 +apply (erule allI [THEN [2] swap])
    2.20 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    2.21 +apply (rule impI)
    2.22 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    2.23 +apply (erule notE)
    2.24 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    2.25 +apply assumption
    2.26 +done
    2.27 +
    2.28 +text {*
    2.29 +@{thm[display] allI [THEN [2] swap]}
    2.30 +*}
    2.31 +
    2.32 +lemma "EX y. ALL x. P(y)-->P(x)"
    2.33 +by blast
    2.34 +
    2.35 +end
    2.36 +
    2.37 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/ZF/IFOL_examples.thy	Tue Aug 19 13:53:58 2003 +0200
     3.3 @@ -0,0 +1,58 @@
     3.4 +header{*Examples of Intuitionistic Reasoning*}
     3.5 +
     3.6 +theory IFOL_examples = IFOL:
     3.7 +
     3.8 +text{*Quantifier example from the book Logic and Computation*}
     3.9 +lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    3.10 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.11 +apply (rule impI)
    3.12 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.13 +apply (rule allI)
    3.14 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.15 +apply (rule exI)
    3.16 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.17 +apply (erule exE)
    3.18 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.19 +apply (erule allE)
    3.20 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.21 +txt{*Now @{text "apply assumption"} fails*}
    3.22 +oops
    3.23 +
    3.24 +text{*Trying again, with the same first two steps*}
    3.25 +lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    3.26 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.27 +apply (rule impI)
    3.28 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.29 +apply (rule allI)
    3.30 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.31 +apply (erule exE)
    3.32 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.33 +apply (rule exI)
    3.34 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.35 +apply (erule allE)
    3.36 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.37 +apply assumption
    3.38 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.39 +done
    3.40 +
    3.41 +lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    3.42 +by (tactic {*IntPr.fast_tac 1*})
    3.43 +
    3.44 +text{*Example of Dyckhoff's method*}
    3.45 +lemma "~ ~ ((P-->Q) | (Q-->P))"
    3.46 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.47 +apply (unfold not_def)
    3.48 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.49 +apply (rule impI)
    3.50 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.51 +apply (erule disj_impE)
    3.52 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.53 +apply (erule imp_impE)
    3.54 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.55 + apply (erule imp_impE)
    3.56 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    3.57 +apply assumption 
    3.58 +apply (erule FalseE)+
    3.59 +done
    3.60 +
    3.61 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/ZF/IsaMakefile	Tue Aug 19 13:53:58 2003 +0200
     4.3 @@ -0,0 +1,50 @@
     4.4 +#
     4.5 +# IsaMakefile to build the examples for the FOL and ZF manual
     4.6 +#
     4.7 +
     4.8 +## targets
     4.9 +
    4.10 +default: ZF-examples styles
    4.11 +images:
    4.12 +test:
    4.13 +all: default
    4.14 +
    4.15 +
    4.16 +## global settings
    4.17 +
    4.18 +SRC = $(ISABELLE_HOME)/src
    4.19 +OUT = $(ISABELLE_OUTPUT)
    4.20 +LOG = $(OUT)/log
    4.21 +OPTIONS = -m brackets -i true -d "" -D document
    4.22 +USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/ZF
    4.23 +
    4.24 +
    4.25 +## ZF
    4.26 +
    4.27 +ZF:
    4.28 +	@cd $(SRC)/ZF; $(ISATOOL) make ZF
    4.29 +
    4.30 +styles:
    4.31 +	@rm -f isabelle.sty
    4.32 +	@rm -f isabellesym.sty
    4.33 +	@rm -f pdfsetup.sty
    4.34 +	@$(ISATOOL) latex -o sty >/dev/null
    4.35 +	@rm -f pdfsetup.sty
    4.36 +	@rm -f document/isabelle.sty
    4.37 +	@rm -f document/isabellesym.sty
    4.38 +	@rm -f document/pdfsetup.sty
    4.39 +	@rm -f document/session.tex
    4.40 +
    4.41 +
    4.42 +## ZF-examples
    4.43 +
    4.44 +ZF-examples: ZF $(LOG)/ZF-examples.gz
    4.45 +
    4.46 +$(LOG)/ZF-examples.gz: $(OUT)/ZF \
    4.47 +	FOL_examples.thy  IFOL_examples.thy ZF_examples.thy If.thy ROOT.ML 
    4.48 +	@$(USEDIR) .
    4.49 +
    4.50 +## clean
    4.51 +
    4.52 +clean:
    4.53 +	@rm -f $(LOG)/ZF-examples.gz document/*.tex 
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/ZF/ROOT.ML	Tue Aug 19 13:53:58 2003 +0200
     5.3 @@ -0,0 +1,5 @@
     5.4 +(* ID:         $Id$ *)
     5.5 +use_thy "IFOL_examples";
     5.6 +use_thy "FOL_examples";
     5.7 +use_thy "ZF_examples";
     5.8 +use_thy "If";
     6.1 --- a/doc-src/ZF/ZF-eg.txt	Fri Aug 15 13:45:39 2003 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,230 +0,0 @@
     6.4 -(**** ZF examples ****)
     6.5 -
     6.6 -Pretty.setmargin 72;  (*existing macros just allow this margin*)
     6.7 -print_depth 0;
     6.8 -
     6.9 -(*** Powerset example ***)
    6.10 -
    6.11 -val [prem] = goal ZF.thy "A<=B  ==>  Pow(A) <= Pow(B)";
    6.12 -by (resolve_tac [subsetI] 1);
    6.13 -by (resolve_tac [PowI] 1);
    6.14 -by (dresolve_tac [PowD] 1);
    6.15 -by (eresolve_tac [subset_trans] 1);
    6.16 -by (resolve_tac [prem] 1);
    6.17 -val Pow_mono = result();
    6.18 -
    6.19 -goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
    6.20 -by (resolve_tac [equalityI] 1);
    6.21 -by (resolve_tac [Int_greatest] 1);
    6.22 -by (resolve_tac [Int_lower1 RS Pow_mono] 1);
    6.23 -by (resolve_tac [Int_lower2 RS Pow_mono] 1);
    6.24 -by (resolve_tac [subsetI] 1);
    6.25 -by (eresolve_tac [IntE] 1);
    6.26 -by (resolve_tac [PowI] 1);
    6.27 -by (REPEAT (dresolve_tac [PowD] 1));
    6.28 -by (resolve_tac [Int_greatest] 1);
    6.29 -by (REPEAT (assume_tac 1));
    6.30 -choplev 0;
    6.31 -by (fast_tac (ZF_cs addIs [equalityI]) 1);
    6.32 -
    6.33 -Goal "C<=D ==> Union(C) <= Union(D)";
    6.34 -by (resolve_tac [subsetI] 1);
    6.35 -by (eresolve_tac [UnionE] 1);
    6.36 -by (resolve_tac [UnionI] 1);
    6.37 -by (eresolve_tac [subsetD] 1);
    6.38 -by (assume_tac 1);
    6.39 -by (assume_tac 1);
    6.40 -choplev 0;
    6.41 -by (resolve_tac [Union_least] 1);
    6.42 -by (resolve_tac [Union_upper] 1);
    6.43 -by (eresolve_tac [subsetD] 1);
    6.44 -
    6.45 -
    6.46 -val prems = goal ZF.thy
    6.47 -    "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
    6.48 -\    (f Un g)`a = f`a";
    6.49 -by (resolve_tac [apply_equality] 1);
    6.50 -by (resolve_tac [UnI1] 1);
    6.51 -by (resolve_tac [apply_Pair] 1);
    6.52 -by (resolve_tac prems 1);
    6.53 -by (resolve_tac prems 1);
    6.54 -by (resolve_tac [fun_disjoint_Un] 1);
    6.55 -by (resolve_tac prems 1);
    6.56 -by (resolve_tac prems 1);
    6.57 -by (resolve_tac prems 1);
    6.58 -
    6.59 -
    6.60 -Goal "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
    6.61 -\     (f Un g)`a = f`a";
    6.62 -by (resolve_tac [apply_equality] 1);
    6.63 -by (resolve_tac [UnI1] 1);
    6.64 -by (resolve_tac [apply_Pair] 1);
    6.65 -by (assume_tac 1);
    6.66 -by (assume_tac 1);
    6.67 -by (resolve_tac [fun_disjoint_Un] 1);
    6.68 -by (assume_tac 1);
    6.69 -by (assume_tac 1);
    6.70 -by (assume_tac 1);
    6.71 -
    6.72 -
    6.73 -
    6.74 -
    6.75 -goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))";
    6.76 -by (resolve_tac [equalityI] 1);
    6.77 -by (resolve_tac [subsetI] 1);
    6.78 -fe imageE;
    6.79 -
    6.80 -
    6.81 -goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x))  Int  B";
    6.82 -by (resolve_tac [equalityI] 1);
    6.83 -by (resolve_tac [Int_greatest] 1);
    6.84 -fr UN_mono;
    6.85 -by (resolve_tac [Int_lower1] 1);
    6.86 -fr UN_least;
    6.87 -????
    6.88 -
    6.89 -
    6.90 -> goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
    6.91 -Level 0
    6.92 -Pow(A Int B) = Pow(A) Int Pow(B)
    6.93 - 1. Pow(A Int B) = Pow(A) Int Pow(B)
    6.94 -> by (resolve_tac [equalityI] 1);
    6.95 -Level 1
    6.96 -Pow(A Int B) = Pow(A) Int Pow(B)
    6.97 - 1. Pow(A Int B) <= Pow(A) Int Pow(B)
    6.98 - 2. Pow(A) Int Pow(B) <= Pow(A Int B)
    6.99 -> by (resolve_tac [Int_greatest] 1);
   6.100 -Level 2
   6.101 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.102 - 1. Pow(A Int B) <= Pow(A)
   6.103 - 2. Pow(A Int B) <= Pow(B)
   6.104 - 3. Pow(A) Int Pow(B) <= Pow(A Int B)
   6.105 -> by (resolve_tac [Int_lower1 RS Pow_mono] 1);
   6.106 -Level 3
   6.107 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.108 - 1. Pow(A Int B) <= Pow(B)
   6.109 - 2. Pow(A) Int Pow(B) <= Pow(A Int B)
   6.110 -> by (resolve_tac [Int_lower2 RS Pow_mono] 1);
   6.111 -Level 4
   6.112 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.113 - 1. Pow(A) Int Pow(B) <= Pow(A Int B)
   6.114 -> by (resolve_tac [subsetI] 1);
   6.115 -Level 5
   6.116 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.117 - 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)
   6.118 -> by (eresolve_tac [IntE] 1);
   6.119 -Level 6
   6.120 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.121 - 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)
   6.122 -> by (resolve_tac [PowI] 1);
   6.123 -Level 7
   6.124 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.125 - 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B
   6.126 -> by (REPEAT (dresolve_tac [PowD] 1));
   6.127 -Level 8
   6.128 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.129 - 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B
   6.130 -> by (resolve_tac [Int_greatest] 1);
   6.131 -Level 9
   6.132 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.133 - 1. !!x. [| x <= A; x <= B |] ==> x <= A
   6.134 - 2. !!x. [| x <= A; x <= B |] ==> x <= B
   6.135 -> by (REPEAT (assume_tac 1));
   6.136 -Level 10
   6.137 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.138 -No subgoals!
   6.139 -> choplev 0;
   6.140 -Level 0
   6.141 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.142 - 1. Pow(A Int B) = Pow(A) Int Pow(B)
   6.143 -> by (fast_tac (ZF_cs addIs [equalityI]) 1);
   6.144 -Level 1
   6.145 -Pow(A Int B) = Pow(A) Int Pow(B)
   6.146 -No subgoals!
   6.147 -
   6.148 -
   6.149 -
   6.150 -
   6.151 -> val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
   6.152 -Level 0
   6.153 -Union(C) <= Union(D)
   6.154 - 1. Union(C) <= Union(D)
   6.155 -> by (resolve_tac [subsetI] 1);
   6.156 -Level 1
   6.157 -Union(C) <= Union(D)
   6.158 - 1. !!x. x : Union(C) ==> x : Union(D)
   6.159 -> by (eresolve_tac [UnionE] 1);
   6.160 -Level 2
   6.161 -Union(C) <= Union(D)
   6.162 - 1. !!x B. [| x : B; B : C |] ==> x : Union(D)
   6.163 -> by (resolve_tac [UnionI] 1);
   6.164 -Level 3
   6.165 -Union(C) <= Union(D)
   6.166 - 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D
   6.167 - 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
   6.168 -> by (resolve_tac [prem RS subsetD] 1);
   6.169 -Level 4
   6.170 -Union(C) <= Union(D)
   6.171 - 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C
   6.172 - 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
   6.173 -> by (assume_tac 1);
   6.174 -Level 5
   6.175 -Union(C) <= Union(D)
   6.176 - 1. !!x B. [| x : B; B : C |] ==> x : B
   6.177 -> by (assume_tac 1);
   6.178 -Level 6
   6.179 -Union(C) <= Union(D)
   6.180 -No subgoals!
   6.181 -
   6.182 -
   6.183 -
   6.184 -> val prems = goal ZF.thy
   6.185 -#     "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
   6.186 -# \    (f Un g)`a = f`a";
   6.187 -Level 0
   6.188 -(f Un g) ` a = f ` a
   6.189 - 1. (f Un g) ` a = f ` a
   6.190 -> by (resolve_tac [apply_equality] 1);
   6.191 -Level 1
   6.192 -(f Un g) ` a = f ` a
   6.193 - 1. <a,f ` a> : f Un g
   6.194 - 2. f Un g : (PROD x:?A. ?B(x))
   6.195 -> by (resolve_tac [UnI1] 1);
   6.196 -Level 2
   6.197 -(f Un g) ` a = f ` a
   6.198 - 1. <a,f ` a> : f
   6.199 - 2. f Un g : (PROD x:?A. ?B(x))
   6.200 -> by (resolve_tac [apply_Pair] 1);
   6.201 -Level 3
   6.202 -(f Un g) ` a = f ` a
   6.203 - 1. f : (PROD x:?A2. ?B2(x))
   6.204 - 2. a : ?A2
   6.205 - 3. f Un g : (PROD x:?A. ?B(x))
   6.206 -> by (resolve_tac prems 1);
   6.207 -Level 4
   6.208 -(f Un g) ` a = f ` a
   6.209 - 1. a : A
   6.210 - 2. f Un g : (PROD x:?A. ?B(x))
   6.211 -> by (resolve_tac prems 1);
   6.212 -Level 5
   6.213 -(f Un g) ` a = f ` a
   6.214 - 1. f Un g : (PROD x:?A. ?B(x))
   6.215 -> by (resolve_tac [fun_disjoint_Un] 1);
   6.216 -Level 6
   6.217 -(f Un g) ` a = f ` a
   6.218 - 1. f : ?A3 -> ?B3
   6.219 - 2. g : ?C3 -> ?D3
   6.220 - 3. ?A3 Int ?C3 = 0
   6.221 -> by (resolve_tac prems 1);
   6.222 -Level 7
   6.223 -(f Un g) ` a = f ` a
   6.224 - 1. g : ?C3 -> ?D3
   6.225 - 2. A Int ?C3 = 0
   6.226 -> by (resolve_tac prems 1);
   6.227 -Level 8
   6.228 -(f Un g) ` a = f ` a
   6.229 - 1. A Int C = 0
   6.230 -> by (resolve_tac prems 1);
   6.231 -Level 9
   6.232 -(f Un g) ` a = f ` a
   6.233 -No subgoals!
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/ZF/ZF_examples.thy	Tue Aug 19 13:53:58 2003 +0200
     7.3 @@ -0,0 +1,121 @@
     7.4 +header{*Examples of Reasoning in ZF Set Theory*}
     7.5 +
     7.6 +theory ZF_examples = Main_ZFC:
     7.7 +
     7.8 +subsection {* Binary Trees *}
     7.9 +
    7.10 +consts
    7.11 +  bt :: "i => i"
    7.12 +
    7.13 +datatype "bt(A)" =
    7.14 +  Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
    7.15 +
    7.16 +declare bt.intros [simp]
    7.17 +
    7.18 +text{*Induction via tactic emulation*}
    7.19 +lemma Br_neq_left [rule_format]: "l \<in> bt(A) ==> \<forall>x r. Br(x, l, r) \<noteq> l"
    7.20 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.21 +  apply (induct_tac l)
    7.22 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.23 +  apply auto
    7.24 +  done
    7.25 +
    7.26 +(*
    7.27 +  apply (Inductive.case_tac l)
    7.28 +  apply (tactic {*exhaust_tac "l" 1*})
    7.29 +*)
    7.30 +
    7.31 +text{*The new induction method, which I don't understand*}
    7.32 +lemma Br_neq_left': "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> l)"
    7.33 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.34 +  apply (induct set: bt)
    7.35 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.36 +  apply auto
    7.37 +  done
    7.38 +
    7.39 +lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
    7.40 +  -- "Proving a freeness theorem."
    7.41 +  by (blast elim!: bt.free_elims)
    7.42 +
    7.43 +inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
    7.44 +  -- "An elimination rule, for type-checking."
    7.45 +
    7.46 +text {*
    7.47 +@{thm[display] BrE[no_vars]}
    7.48 +\rulename{BrE}
    7.49 +*};
    7.50 +
    7.51 +subsection{*Powerset example*}
    7.52 +
    7.53 +lemma Pow_mono: "A<=B  ==>  Pow(A) <= Pow(B)"
    7.54 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.55 +apply (rule subsetI)
    7.56 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.57 +apply (rule PowI)
    7.58 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.59 +apply (drule PowD)
    7.60 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.61 +apply (erule subset_trans, assumption)
    7.62 +done
    7.63 +
    7.64 +lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
    7.65 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.66 +apply (rule equalityI)
    7.67 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.68 +apply (rule Int_greatest)
    7.69 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.70 +apply (rule Int_lower1 [THEN Pow_mono])
    7.71 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.72 +apply (rule Int_lower2 [THEN Pow_mono])
    7.73 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.74 +apply (rule subsetI)
    7.75 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.76 +apply (erule IntE)
    7.77 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.78 +apply (rule PowI)
    7.79 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.80 +apply (drule PowD)+
    7.81 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.82 +apply (rule Int_greatest, assumption+)
    7.83 +done
    7.84 +
    7.85 +text{*Trying again from the beginning in order to use @{text blast}*}
    7.86 +lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
    7.87 +by blast
    7.88 +
    7.89 +
    7.90 +lemma "C<=D ==> Union(C) <= Union(D)"
    7.91 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.92 +apply (rule subsetI)
    7.93 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.94 +apply (erule UnionE)
    7.95 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.96 +apply (rule UnionI)
    7.97 +apply (erule subsetD, assumption, assumption)
    7.98 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    7.99 +done
   7.100 +
   7.101 +text{*Trying again from the beginning in order to prove from the definitions*}
   7.102 +
   7.103 +lemma "C<=D ==> Union(C) <= Union(D)"
   7.104 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   7.105 +apply (rule Union_least)
   7.106 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   7.107 +apply (rule Union_upper)
   7.108 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   7.109 +apply (erule subsetD, assumption)
   7.110 +done
   7.111 +
   7.112 +
   7.113 +lemma "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==> (f Un g)`a = f`a"
   7.114 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   7.115 +apply (rule apply_equality)
   7.116 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   7.117 +apply (rule UnI1)
   7.118 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   7.119 +apply (rule apply_Pair, assumption+)
   7.120 +  --{* @{subgoals[display,indent=0,margin=65]} *}
   7.121 +apply (rule fun_disjoint_Un, assumption+)
   7.122 +done
   7.123 +
   7.124 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/ZF/isabelle.sty	Tue Aug 19 13:53:58 2003 +0200
     8.3 @@ -0,0 +1,157 @@
     8.4 +%%
     8.5 +%% Author: Markus Wenzel, TU Muenchen
     8.6 +%% License: GPL (GNU GENERAL PUBLIC LICENSE)
     8.7 +%%
     8.8 +%% macros for Isabelle generated LaTeX output
     8.9 +%%
    8.10 +
    8.11 +%%% Simple document preparation (based on theory token language and symbols)
    8.12 +
    8.13 +% isabelle environments
    8.14 +
    8.15 +\newcommand{\isabellecontext}{UNKNOWN}
    8.16 +
    8.17 +\newcommand{\isastyle}{\small\tt\slshape}
    8.18 +\newcommand{\isastyleminor}{\small\tt\slshape}
    8.19 +\newcommand{\isastylescript}{\footnotesize\tt\slshape}
    8.20 +\newcommand{\isastyletext}{\normalsize\rm}
    8.21 +\newcommand{\isastyletxt}{\rm}
    8.22 +\newcommand{\isastylecmt}{\rm}
    8.23 +
    8.24 +%symbol markup -- \emph achieves decent spacing via italic corrections
    8.25 +\newcommand{\isamath}[1]{\emph{$#1$}}
    8.26 +\newcommand{\isatext}[1]{\emph{#1}}
    8.27 +\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    8.28 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    8.29 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    8.30 +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    8.31 +
    8.32 +\newdimen\isa@parindent\newdimen\isa@parskip
    8.33 +
    8.34 +\newenvironment{isabellebody}{%
    8.35 +\isamarkuptrue\par%
    8.36 +\isa@parindent\parindent\parindent0pt%
    8.37 +\isa@parskip\parskip\parskip0pt%
    8.38 +\isastyle}{\par}
    8.39 +
    8.40 +\newenvironment{isabelle}
    8.41 +{\begin{trivlist}\begin{isabellebody}\item\relax}
    8.42 +{\end{isabellebody}\end{trivlist}}
    8.43 +
    8.44 +\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
    8.45 +
    8.46 +\newcommand{\isaindent}[1]{\hphantom{#1}}
    8.47 +\newcommand{\isanewline}{\mbox{}\par\mbox{}}
    8.48 +\newcommand{\isadigit}[1]{#1}
    8.49 +
    8.50 +\chardef\isacharbang=`\!
    8.51 +\chardef\isachardoublequote=`\"
    8.52 +\chardef\isacharhash=`\#
    8.53 +\chardef\isachardollar=`\$
    8.54 +\chardef\isacharpercent=`\%
    8.55 +\chardef\isacharampersand=`\&
    8.56 +\chardef\isacharprime=`\'
    8.57 +\chardef\isacharparenleft=`\(
    8.58 +\chardef\isacharparenright=`\)
    8.59 +\chardef\isacharasterisk=`\*
    8.60 +\chardef\isacharplus=`\+
    8.61 +\chardef\isacharcomma=`\,
    8.62 +\chardef\isacharminus=`\-
    8.63 +\chardef\isachardot=`\.
    8.64 +\chardef\isacharslash=`\/
    8.65 +\chardef\isacharcolon=`\:
    8.66 +\chardef\isacharsemicolon=`\;
    8.67 +\chardef\isacharless=`\<
    8.68 +\chardef\isacharequal=`\=
    8.69 +\chardef\isachargreater=`\>
    8.70 +\chardef\isacharquery=`\?
    8.71 +\chardef\isacharat=`\@
    8.72 +\chardef\isacharbrackleft=`\[
    8.73 +\chardef\isacharbackslash=`\\
    8.74 +\chardef\isacharbrackright=`\]
    8.75 +\chardef\isacharcircum=`\^
    8.76 +\chardef\isacharunderscore=`\_
    8.77 +\chardef\isacharbackquote=`\`
    8.78 +\chardef\isacharbraceleft=`\{
    8.79 +\chardef\isacharbar=`\|
    8.80 +\chardef\isacharbraceright=`\}
    8.81 +\chardef\isachartilde=`\~
    8.82 +
    8.83 +
    8.84 +% keyword and section markup
    8.85 +
    8.86 +\newcommand{\isakeywordcharunderscore}{\_}
    8.87 +\newcommand{\isakeyword}[1]
    8.88 +{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
    8.89 +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
    8.90 +\newcommand{\isacommand}[1]{\isakeyword{#1}}
    8.91 +
    8.92 +\newcommand{\isamarkupheader}[1]{\section{#1}}
    8.93 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
    8.94 +\newcommand{\isamarkupsection}[1]{\section{#1}}
    8.95 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
    8.96 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
    8.97 +\newcommand{\isamarkupsect}[1]{\section{#1}}
    8.98 +\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
    8.99 +\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
   8.100 +
   8.101 +\newif\ifisamarkup
   8.102 +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
   8.103 +\newcommand{\isaendpar}{\par\medskip}
   8.104 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
   8.105 +\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
   8.106 +\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
   8.107 +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   8.108 +
   8.109 +
   8.110 +% alternative styles
   8.111 +
   8.112 +\newcommand{\isabellestyle}{}
   8.113 +\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
   8.114 +
   8.115 +\newcommand{\isabellestylett}{%
   8.116 +\renewcommand{\isastyle}{\small\tt}%
   8.117 +\renewcommand{\isastyleminor}{\small\tt}%
   8.118 +\renewcommand{\isastylescript}{\footnotesize\tt}%
   8.119 +}
   8.120 +\newcommand{\isabellestyleit}{%
   8.121 +\renewcommand{\isastyle}{\small\it}%
   8.122 +\renewcommand{\isastyleminor}{\it}%
   8.123 +\renewcommand{\isastylescript}{\footnotesize\it}%
   8.124 +\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
   8.125 +\renewcommand{\isacharbang}{\isamath{!}}%
   8.126 +\renewcommand{\isachardoublequote}{}%
   8.127 +\renewcommand{\isacharhash}{\isamath{\#}}%
   8.128 +\renewcommand{\isachardollar}{\isamath{\$}}%
   8.129 +\renewcommand{\isacharpercent}{\isamath{\%}}%
   8.130 +\renewcommand{\isacharampersand}{\isamath{\&}}%
   8.131 +\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
   8.132 +\renewcommand{\isacharparenleft}{\isamath{(}}%
   8.133 +\renewcommand{\isacharparenright}{\isamath{)}}%
   8.134 +\renewcommand{\isacharasterisk}{\isamath{*}}%
   8.135 +\renewcommand{\isacharplus}{\isamath{+}}%
   8.136 +\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
   8.137 +\renewcommand{\isacharminus}{\isamath{-}}%
   8.138 +\renewcommand{\isachardot}{\isamath{\mathord.}}%
   8.139 +\renewcommand{\isacharslash}{\isamath{/}}%
   8.140 +\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
   8.141 +\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
   8.142 +\renewcommand{\isacharless}{\isamath{<}}%
   8.143 +\renewcommand{\isacharequal}{\isamath{=}}%
   8.144 +\renewcommand{\isachargreater}{\isamath{>}}%
   8.145 +\renewcommand{\isacharat}{\isamath{@}}%
   8.146 +\renewcommand{\isacharbrackleft}{\isamath{[}}%
   8.147 +\renewcommand{\isacharbrackright}{\isamath{]}}%
   8.148 +\renewcommand{\isacharunderscore}{\mbox{-}}%
   8.149 +\renewcommand{\isacharbraceleft}{\isamath{\{}}%
   8.150 +\renewcommand{\isacharbar}{\isamath{\mid}}%
   8.151 +\renewcommand{\isacharbraceright}{\isamath{\}}}%
   8.152 +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
   8.153 +}
   8.154 +
   8.155 +\newcommand{\isabellestylesl}{%
   8.156 +\isabellestyleit%
   8.157 +\renewcommand{\isastyle}{\small\sl}%
   8.158 +\renewcommand{\isastyleminor}{\sl}%
   8.159 +\renewcommand{\isastylescript}{\footnotesize\sl}%
   8.160 +}
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/ZF/isabellesym.sty	Tue Aug 19 13:53:58 2003 +0200
     9.3 @@ -0,0 +1,354 @@
     9.4 +%%
     9.5 +%% Author: Markus Wenzel, TU Muenchen
     9.6 +%% License: GPL (GNU GENERAL PUBLIC LICENSE)
     9.7 +%%
     9.8 +%% definitions of standard Isabelle symbols
     9.9 +%%
    9.10 +
    9.11 +% symbol definitions
    9.12 +
    9.13 +\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssym
    9.14 +\newcommand{\isasymone}{\isamath{\mathbf{1}}}   %requires amssym
    9.15 +\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}   %requires amssym
    9.16 +\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssym
    9.17 +\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssym
    9.18 +\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssym
    9.19 +\newcommand{\isasymsix}{\isamath{\mathbf{6}}}   %requires amssym
    9.20 +\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssym
    9.21 +\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssym
    9.22 +\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssym
    9.23 +\newcommand{\isasymA}{\isamath{\mathcal{A}}}
    9.24 +\newcommand{\isasymB}{\isamath{\mathcal{B}}}
    9.25 +\newcommand{\isasymC}{\isamath{\mathcal{C}}}
    9.26 +\newcommand{\isasymD}{\isamath{\mathcal{D}}}
    9.27 +\newcommand{\isasymE}{\isamath{\mathcal{E}}}
    9.28 +\newcommand{\isasymF}{\isamath{\mathcal{F}}}
    9.29 +\newcommand{\isasymG}{\isamath{\mathcal{G}}}
    9.30 +\newcommand{\isasymH}{\isamath{\mathcal{H}}}
    9.31 +\newcommand{\isasymI}{\isamath{\mathcal{I}}}
    9.32 +\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
    9.33 +\newcommand{\isasymK}{\isamath{\mathcal{K}}}
    9.34 +\newcommand{\isasymL}{\isamath{\mathcal{L}}}
    9.35 +\newcommand{\isasymM}{\isamath{\mathcal{M}}}
    9.36 +\newcommand{\isasymN}{\isamath{\mathcal{N}}}
    9.37 +\newcommand{\isasymO}{\isamath{\mathcal{O}}}
    9.38 +\newcommand{\isasymP}{\isamath{\mathcal{P}}}
    9.39 +\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
    9.40 +\newcommand{\isasymR}{\isamath{\mathcal{R}}}
    9.41 +\newcommand{\isasymS}{\isamath{\mathcal{S}}}
    9.42 +\newcommand{\isasymT}{\isamath{\mathcal{T}}}
    9.43 +\newcommand{\isasymU}{\isamath{\mathcal{U}}}
    9.44 +\newcommand{\isasymV}{\isamath{\mathcal{V}}}
    9.45 +\newcommand{\isasymW}{\isamath{\mathcal{W}}}
    9.46 +\newcommand{\isasymX}{\isamath{\mathcal{X}}}
    9.47 +\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
    9.48 +\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
    9.49 +\newcommand{\isasyma}{\isamath{\mathrm{a}}}
    9.50 +\newcommand{\isasymb}{\isamath{\mathrm{b}}}
    9.51 +\newcommand{\isasymc}{\isamath{\mathrm{c}}}
    9.52 +\newcommand{\isasymd}{\isamath{\mathrm{d}}}
    9.53 +\newcommand{\isasyme}{\isamath{\mathrm{e}}}
    9.54 +\newcommand{\isasymf}{\isamath{\mathrm{f}}}
    9.55 +\newcommand{\isasymg}{\isamath{\mathrm{g}}}
    9.56 +\newcommand{\isasymh}{\isamath{\mathrm{h}}}
    9.57 +\newcommand{\isasymi}{\isamath{\mathrm{i}}}
    9.58 +\newcommand{\isasymj}{\isamath{\mathrm{j}}}
    9.59 +\newcommand{\isasymk}{\isamath{\mathrm{k}}}
    9.60 +\newcommand{\isasyml}{\isamath{\mathrm{l}}}
    9.61 +\newcommand{\isasymm}{\isamath{\mathrm{m}}}
    9.62 +\newcommand{\isasymn}{\isamath{\mathrm{n}}}
    9.63 +\newcommand{\isasymo}{\isamath{\mathrm{o}}}
    9.64 +\newcommand{\isasymp}{\isamath{\mathrm{p}}}
    9.65 +\newcommand{\isasymq}{\isamath{\mathrm{q}}}
    9.66 +\newcommand{\isasymr}{\isamath{\mathrm{r}}}
    9.67 +\newcommand{\isasyms}{\isamath{\mathrm{s}}}
    9.68 +\newcommand{\isasymt}{\isamath{\mathrm{t}}}
    9.69 +\newcommand{\isasymu}{\isamath{\mathrm{u}}}
    9.70 +\newcommand{\isasymv}{\isamath{\mathrm{v}}}
    9.71 +\newcommand{\isasymw}{\isamath{\mathrm{w}}}
    9.72 +\newcommand{\isasymx}{\isamath{\mathrm{x}}}
    9.73 +\newcommand{\isasymy}{\isamath{\mathrm{y}}}
    9.74 +\newcommand{\isasymz}{\isamath{\mathrm{z}}}
    9.75 +\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
    9.76 +\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
    9.77 +\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
    9.78 +\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
    9.79 +\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
    9.80 +\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
    9.81 +\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
    9.82 +\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
    9.83 +\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
    9.84 +\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
    9.85 +\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
    9.86 +\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
    9.87 +\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
    9.88 +\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
    9.89 +\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
    9.90 +\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
    9.91 +\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
    9.92 +\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
    9.93 +\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
    9.94 +\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
    9.95 +\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
    9.96 +\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
    9.97 +\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
    9.98 +\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
    9.99 +\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
   9.100 +\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
   9.101 +\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
   9.102 +\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
   9.103 +\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
   9.104 +\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
   9.105 +\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
   9.106 +\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
   9.107 +\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
   9.108 +\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
   9.109 +\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
   9.110 +\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
   9.111 +\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
   9.112 +\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
   9.113 +\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
   9.114 +\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
   9.115 +\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
   9.116 +\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
   9.117 +\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
   9.118 +\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
   9.119 +\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
   9.120 +\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
   9.121 +\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
   9.122 +\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
   9.123 +\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
   9.124 +\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
   9.125 +\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
   9.126 +\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
   9.127 +\newcommand{\isasymalpha}{\isamath{\alpha}}
   9.128 +\newcommand{\isasymbeta}{\isamath{\beta}}
   9.129 +\newcommand{\isasymgamma}{\isamath{\gamma}}
   9.130 +\newcommand{\isasymdelta}{\isamath{\delta}}
   9.131 +\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
   9.132 +\newcommand{\isasymzeta}{\isamath{\zeta}}
   9.133 +\newcommand{\isasymeta}{\isamath{\eta}}
   9.134 +\newcommand{\isasymtheta}{\isamath{\vartheta}}
   9.135 +\newcommand{\isasymiota}{\isamath{\iota}}
   9.136 +\newcommand{\isasymkappa}{\isamath{\kappa}}
   9.137 +\newcommand{\isasymlambda}{\isamath{\lambda}}
   9.138 +\newcommand{\isasymmu}{\isamath{\mu}}
   9.139 +\newcommand{\isasymnu}{\isamath{\nu}}
   9.140 +\newcommand{\isasymxi}{\isamath{\xi}}
   9.141 +\newcommand{\isasympi}{\isamath{\pi}}
   9.142 +\newcommand{\isasymrho}{\isamath{\varrho}}
   9.143 +\newcommand{\isasymsigma}{\isamath{\sigma}}
   9.144 +\newcommand{\isasymtau}{\isamath{\tau}}
   9.145 +\newcommand{\isasymupsilon}{\isamath{\upsilon}}
   9.146 +\newcommand{\isasymphi}{\isamath{\varphi}}
   9.147 +\newcommand{\isasymchi}{\isamath{\chi}}
   9.148 +\newcommand{\isasympsi}{\isamath{\psi}}
   9.149 +\newcommand{\isasymomega}{\isamath{\omega}}
   9.150 +\newcommand{\isasymGamma}{\isamath{\Gamma}}
   9.151 +\newcommand{\isasymDelta}{\isamath{\Delta}}
   9.152 +\newcommand{\isasymTheta}{\isamath{\Theta}}
   9.153 +\newcommand{\isasymLambda}{\isamath{\Lambda}}
   9.154 +\newcommand{\isasymXi}{\isamath{\Xi}}
   9.155 +\newcommand{\isasymPi}{\isamath{\Pi}}
   9.156 +\newcommand{\isasymSigma}{\isamath{\Sigma}}
   9.157 +\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
   9.158 +\newcommand{\isasymPhi}{\isamath{\Phi}}
   9.159 +\newcommand{\isasymPsi}{\isamath{\Psi}}
   9.160 +\newcommand{\isasymOmega}{\isamath{\Omega}}
   9.161 +\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
   9.162 +\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
   9.163 +\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
   9.164 +\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
   9.165 +\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
   9.166 +\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
   9.167 +\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
   9.168 +\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
   9.169 +\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
   9.170 +\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
   9.171 +\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
   9.172 +\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
   9.173 +\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
   9.174 +\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
   9.175 +\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
   9.176 +\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
   9.177 +\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
   9.178 +\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
   9.179 +\newcommand{\isasymmapsto}{\isamath{\mapsto}}
   9.180 +\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
   9.181 +\newcommand{\isasymmidarrow}{\isamath{\relbar}}
   9.182 +\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
   9.183 +\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
   9.184 +\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
   9.185 +\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
   9.186 +\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
   9.187 +\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
   9.188 +\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
   9.189 +\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
   9.190 +\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssym
   9.191 +\newcommand{\isasymup}{\isamath{\uparrow}}
   9.192 +\newcommand{\isasymUp}{\isamath{\Uparrow}}
   9.193 +\newcommand{\isasymdown}{\isamath{\downarrow}}
   9.194 +\newcommand{\isasymDown}{\isamath{\Downarrow}}
   9.195 +\newcommand{\isasymupdown}{\isamath{\updownarrow}}
   9.196 +\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
   9.197 +\newcommand{\isasymlangle}{\isamath{\langle}}
   9.198 +\newcommand{\isasymrangle}{\isamath{\rangle}}
   9.199 +\newcommand{\isasymlceil}{\isamath{\lceil}}
   9.200 +\newcommand{\isasymrceil}{\isamath{\rceil}}
   9.201 +\newcommand{\isasymlfloor}{\isamath{\lfloor}}
   9.202 +\newcommand{\isasymrfloor}{\isamath{\rfloor}}
   9.203 +\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
   9.204 +\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
   9.205 +\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
   9.206 +\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
   9.207 +\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
   9.208 +\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
   9.209 +\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel 
   9.210 +\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel 
   9.211 +\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
   9.212 +\newcommand{\isasymnot}{\isamath{\neg}}
   9.213 +\newcommand{\isasymbottom}{\isamath{\bot}}
   9.214 +\newcommand{\isasymtop}{\isamath{\top}}
   9.215 +\newcommand{\isasymand}{\isamath{\wedge}}
   9.216 +\newcommand{\isasymAnd}{\isamath{\bigwedge}}
   9.217 +\newcommand{\isasymor}{\isamath{\vee}}
   9.218 +\newcommand{\isasymOr}{\isamath{\bigvee}}
   9.219 +\newcommand{\isasymforall}{\isamath{\forall\,}}
   9.220 +\newcommand{\isasymexists}{\isamath{\exists\,}}
   9.221 +\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssym
   9.222 +\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssym
   9.223 +\newcommand{\isasymturnstile}{\isamath{\vdash}}
   9.224 +\newcommand{\isasymTurnstile}{\isamath{\models}}
   9.225 +\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
   9.226 +\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
   9.227 +\newcommand{\isasymstileturn}{\isamath{\dashv}}
   9.228 +\newcommand{\isasymsurd}{\isamath{\surd}}
   9.229 +\newcommand{\isasymle}{\isamath{\le}}
   9.230 +\newcommand{\isasymge}{\isamath{\ge}}
   9.231 +\newcommand{\isasymlless}{\isamath{\ll}}
   9.232 +\newcommand{\isasymggreater}{\isamath{\gg}}
   9.233 +\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
   9.234 +\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
   9.235 +\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
   9.236 +\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
   9.237 +\newcommand{\isasymin}{\isamath{\in}}
   9.238 +\newcommand{\isasymnotin}{\isamath{\notin}}
   9.239 +\newcommand{\isasymsubset}{\isamath{\subset}}
   9.240 +\newcommand{\isasymsupset}{\isamath{\supset}}
   9.241 +\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
   9.242 +\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
   9.243 +\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
   9.244 +\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssym
   9.245 +\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
   9.246 +\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
   9.247 +\newcommand{\isasyminter}{\isamath{\cap}}
   9.248 +\newcommand{\isasymInter}{\isamath{\bigcap\,}}
   9.249 +\newcommand{\isasymunion}{\isamath{\cup}}
   9.250 +\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
   9.251 +\newcommand{\isasymsqunion}{\isamath{\sqcup}}
   9.252 +\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
   9.253 +\newcommand{\isasymsqinter}{\isamath{\sqcap}}
   9.254 +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires masmath
   9.255 +\newcommand{\isasymuplus}{\isamath{\uplus}}
   9.256 +\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
   9.257 +\newcommand{\isasymnoteq}{\isamath{\not=}}
   9.258 +\newcommand{\isasymsim}{\isamath{\sim}}
   9.259 +\newcommand{\isasymdoteq}{\isamath{\doteq}}
   9.260 +\newcommand{\isasymsimeq}{\isamath{\simeq}}
   9.261 +\newcommand{\isasymapprox}{\isamath{\approx}}
   9.262 +\newcommand{\isasymasymp}{\isamath{\asymp}}
   9.263 +\newcommand{\isasymcong}{\isamath{\cong}}
   9.264 +\newcommand{\isasymsmile}{\isamath{\smile}}
   9.265 +\newcommand{\isasymequiv}{\isamath{\equiv}}
   9.266 +\newcommand{\isasymfrown}{\isamath{\frown}}
   9.267 +\newcommand{\isasympropto}{\isamath{\propto}}
   9.268 +\newcommand{\isasymbowtie}{\isamath{\bowtie}}
   9.269 +\newcommand{\isasymprec}{\isamath{\prec}}
   9.270 +\newcommand{\isasymsucc}{\isamath{\succ}}
   9.271 +\newcommand{\isasympreceq}{\isamath{\preceq}}
   9.272 +\newcommand{\isasymsucceq}{\isamath{\succeq}}
   9.273 +\newcommand{\isasymparallel}{\isamath{\parallel}}
   9.274 +\newcommand{\isasymbar}{\isamath{\mid}}
   9.275 +\newcommand{\isasymplusminus}{\isamath{\pm}}
   9.276 +\newcommand{\isasymminusplus}{\isamath{\mp}}
   9.277 +\newcommand{\isasymtimes}{\isamath{\times}}
   9.278 +\newcommand{\isasymdiv}{\isamath{\div}}
   9.279 +\newcommand{\isasymcdot}{\isamath{\cdot}}
   9.280 +\newcommand{\isasymstar}{\isamath{\star}}
   9.281 +\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
   9.282 +\newcommand{\isasymcirc}{\isamath{\circ}}
   9.283 +\newcommand{\isasymdagger}{\isamath{\dagger}}
   9.284 +\newcommand{\isasymddagger}{\isamath{\ddagger}}
   9.285 +\newcommand{\isasymlhd}{\isamath{\lhd}}
   9.286 +\newcommand{\isasymrhd}{\isamath{\rhd}}
   9.287 +\newcommand{\isasymunlhd}{\isamath{\unlhd}}
   9.288 +\newcommand{\isasymunrhd}{\isamath{\unrhd}}
   9.289 +\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
   9.290 +\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
   9.291 +\newcommand{\isasymtriangle}{\isamath{\triangle}}
   9.292 +\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
   9.293 +\newcommand{\isasymoplus}{\isamath{\oplus}}
   9.294 +\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
   9.295 +\newcommand{\isasymotimes}{\isamath{\otimes}}
   9.296 +\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
   9.297 +\newcommand{\isasymodot}{\isamath{\odot}}
   9.298 +\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
   9.299 +\newcommand{\isasymominus}{\isamath{\ominus}}
   9.300 +\newcommand{\isasymoslash}{\isamath{\oslash}}
   9.301 +\newcommand{\isasymdots}{\isamath{\dots}}
   9.302 +\newcommand{\isasymcdots}{\isamath{\cdots}}
   9.303 +\newcommand{\isasymSum}{\isamath{\sum\,}}
   9.304 +\newcommand{\isasymProd}{\isamath{\prod\,}}
   9.305 +\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
   9.306 +\newcommand{\isasyminfinity}{\isamath{\infty}}
   9.307 +\newcommand{\isasymintegral}{\isamath{\int\,}}
   9.308 +\newcommand{\isasymointegral}{\isamath{\oint\,}}
   9.309 +\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
   9.310 +\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
   9.311 +\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
   9.312 +\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
   9.313 +\newcommand{\isasymaleph}{\isamath{\aleph}}
   9.314 +\newcommand{\isasymemptyset}{\isamath{\emptyset}}
   9.315 +\newcommand{\isasymnabla}{\isamath{\nabla}}
   9.316 +\newcommand{\isasympartial}{\isamath{\partial}}
   9.317 +\newcommand{\isasymRe}{\isamath{\Re}}
   9.318 +\newcommand{\isasymIm}{\isamath{\Im}}
   9.319 +\newcommand{\isasymflat}{\isamath{\flat}}
   9.320 +\newcommand{\isasymnatural}{\isamath{\natural}}
   9.321 +\newcommand{\isasymsharp}{\isamath{\sharp}}
   9.322 +\newcommand{\isasymangle}{\isamath{\angle}}
   9.323 +\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
   9.324 +\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
   9.325 +\newcommand{\isasymhyphen}{\isatext{\rm-}}
   9.326 +\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
   9.327 +\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}}  %requires latin1
   9.328 +\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires latin1
   9.329 +\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}}  %requires latin1
   9.330 +\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires latin1
   9.331 +\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}}  %requires latin1
   9.332 +\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires latin1
   9.333 +\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
   9.334 +\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
   9.335 +\newcommand{\isasymsection}{\isatext{\rm\S}}
   9.336 +\newcommand{\isasymparagraph}{\isatext{\rm\P}}
   9.337 +\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
   9.338 +\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
   9.339 +\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}}  %requires greek babel
   9.340 +\newcommand{\isasympounds}{\isamath{\pounds}}
   9.341 +\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
   9.342 +\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
   9.343 +\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
   9.344 +\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
   9.345 +\newcommand{\isasymamalg}{\isamath{\amalg}}
   9.346 +\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssym
   9.347 +\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
   9.348 +\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssym
   9.349 +\newcommand{\isasymwp}{\isamath{\wp}}
   9.350 +\newcommand{\isasymwrong}{\isamath{\wr}}
   9.351 +\newcommand{\isasymstruct}{\isamath{\diamond}}
   9.352 +\newcommand{\isasymacute}{\isatext{\'\relax}}
   9.353 +\newcommand{\isasymindex}{\isatext{\i}}
   9.354 +\newcommand{\isasymdieresis}{\isatext{\"\relax}}
   9.355 +\newcommand{\isasymcedilla}{\isatext{\c\relax}}
   9.356 +\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
   9.357 +\newcommand{\isasymspacespace}{\isamath{~~}}