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