src/HOL/Real/HahnBanach/FunctionOrder.thy
 changeset 9408 d3d56e1d2ec1 parent 9379 21cfeae6659d child 9503 3324cbbecef8
```     1.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sun Jul 23 11:59:21 2000 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sun Jul 23 12:01:05 2000 +0200
1.3 @@ -24,16 +24,16 @@
1.4    graph :: "['a set, 'a => real] => 'a graph "
1.5    "graph F f == {(x, f x) | x. x \\<in> F}"
1.6
1.7 -lemma graphI [intro??]: "x \\<in> F ==> (x, f x) \\<in> graph F f"
1.8 +lemma graphI [intro?]: "x \\<in> F ==> (x, f x) \\<in> graph F f"
1.9    by (unfold graph_def, intro CollectI exI) force
1.10
1.11 -lemma graphI2 [intro??]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)"
1.12 +lemma graphI2 [intro?]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)"
1.13    by (unfold graph_def, force)
1.14
1.15 -lemma graphD1 [intro??]: "(x, y) \\<in> graph F f ==> x \\<in> F"
1.16 +lemma graphD1 [intro?]: "(x, y) \\<in> graph F f ==> x \\<in> F"
1.17    by (unfold graph_def, elim CollectE exE) force
1.18
1.19 -lemma graphD2 [intro??]: "(x, y) \\<in> graph H h ==> y = h x"
1.20 +lemma graphD2 [intro?]: "(x, y) \\<in> graph H h ==> y = h x"
1.21    by (unfold graph_def, elim CollectE exE) force
1.22
1.23  subsection {* Functions ordered by domain extension *}
1.24 @@ -46,11 +46,11 @@
1.25    ==> graph H h <= graph H' h'"
1.26    by (unfold graph_def, force)
1.27
1.28 -lemma graph_extD1 [intro??]:
1.29 +lemma graph_extD1 [intro?]:
1.30    "[| graph H h <= graph H' h'; x \\<in> H |] ==> h x = h' x"
1.31    by (unfold graph_def, force)
1.32
1.33 -lemma graph_extD2 [intro??]:
1.34 +lemma graph_extD2 [intro?]:
1.35    "[| graph H h <= graph H' h' |] ==> H <= H'"
1.36    by (unfold graph_def, force)
1.37
```