src/HOL/MicroJava/J/State.ML
changeset 10042 7164dc0d24d8
parent 9970 dfe4747c8318
child 10613 78b1d6c3ee9c
     1.1 --- a/src/HOL/MicroJava/J/State.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/State.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  Addsimps [obj_ty_def2];
     1.5  
     1.6  val new_AddrD = prove_goalw thy [new_Addr_def] 
     1.7 -"\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and>  x = None |  x = Some OutOfMemory" (K[
     1.8 +"!!X. (a,x) = new_Addr h ==> h a = None \\<and>  x = None |  x = Some OutOfMemory" (K[
     1.9  	asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
    1.10  	rtac someI 1,
    1.11  	rtac disjI2 1,
    1.12 @@ -40,20 +40,20 @@
    1.13  Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2,if_None_eq];
    1.14  
    1.15  val raise_if_SomeD = prove_goalw thy [raise_if_def] 
    1.16 -	"raise_if c x y = Some z \\<longrightarrow> c \\<and>  Some z = Some x |  y = Some z" 
    1.17 +	"raise_if c x y = Some z --> c \\<and>  Some z = Some x |  y = Some z" 
    1.18  (K [split_tac [split_if] 1,Auto_tac]) RS mp;
    1.19  
    1.20  val raise_if_NoneD = prove_goalw thy [raise_if_def] 
    1.21 -	"raise_if c x y = None \\<longrightarrow> \\<not> c \\<and>  y = None"
    1.22 +	"raise_if c x y = None --> \\<not> c \\<and>  y = None"
    1.23  (K [split_tac [split_if] 1,Auto_tac]) RS mp;
    1.24  
    1.25  
    1.26  val np_NoneD = (prove_goalw thy [np_def, raise_if_def] 
    1.27 -	"np a' x' = None \\<longrightarrow> x' = None \\<and>  a' \\<noteq> Null" (fn _ => [
    1.28 +	"np a' x' = None --> x' = None \\<and>  a' \\<noteq> Null" (fn _ => [
    1.29  	split_tac [split_if] 1,
    1.30  	Auto_tac ])) RS mp;
    1.31  val np_None = (prove_goalw thy [np_def, raise_if_def] 
    1.32 -	"a' \\<noteq> Null \\<longrightarrow> np a' x' = x'" (fn _ => [
    1.33 +	"a' \\<noteq> Null --> np a' x' = x'" (fn _ => [
    1.34  	split_tac [split_if] 1,
    1.35  	Auto_tac ])) RS mp;
    1.36  val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"