src/HOL/MicroJava/J/Example.ML
changeset 10042 7164dc0d24d8
parent 9348 f495dba0cb07
child 10138 412a3ced6efd
     1.1 --- a/src/HOL/MicroJava/J/Example.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Example.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"] 
     1.5  "map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]);
     1.6  val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"] 
     1.7 -"\\<And>X. x\\<noteq>k \\<Longrightarrow> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
     1.8 +"!!X. x\\<noteq>k ==> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
     1.9  Delsimps[map_of_Cons]; (* sic! *)
    1.10  Addsimps[map_of_Cons1, map_of_Cons2];
    1.11  
    1.12 @@ -30,12 +30,12 @@
    1.13  	Simp_tac 1]);
    1.14  Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];
    1.15  
    1.16 -Goal "\\<And>X. (Object,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
    1.17 +Goal "!!X. (Object,C) \\<in> (subcls1 tprg)^+ ==> R";
    1.18  by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
    1.19  qed "not_Object_subcls";
    1.20  AddSEs [not_Object_subcls];
    1.21  
    1.22 -Goal "tprg\\<turnstile>Object\\<preceq>C C \\<Longrightarrow> C = Object";
    1.23 +Goal "tprg\\<turnstile>Object\\<preceq>C C ==> C = Object";
    1.24  be rtrancl_induct 1;
    1.25  by  Auto_tac;
    1.26  bd subcls1D 1;
    1.27 @@ -43,16 +43,16 @@
    1.28  qed "subcls_ObjectD";
    1.29  AddSDs[subcls_ObjectD];
    1.30  
    1.31 -Goal "\\<And>X. (Base, Ext) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
    1.32 +Goal "!!X. (Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
    1.33  by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
    1.34  qed "not_Base_subcls_Ext";
    1.35  AddSEs [not_Base_subcls_Ext];
    1.36  
    1.37 -Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z \\<Longrightarrow> C=Object \\<or> C=Base \\<or> C=Ext";
    1.38 +Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
    1.39  by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm]));
    1.40  qed "class_tprgD";
    1.41  
    1.42 -Goal "(C,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
    1.43 +Goal "(C,C) \\<in> (subcls1 tprg)^+ ==> R";
    1.44  by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
    1.45  by (ftac class_tprgD 1);
    1.46  by (auto_tac (claset() addSDs [],simpset()));
    1.47 @@ -196,7 +196,7 @@
    1.48  
    1.49  fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
    1.50  Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\ 
    1.51 -\ Expr(e\\<Colon>=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
    1.52 +\ Expr(e::=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
    1.53  (* ?pTs' = [Class Base] *)
    1.54  by t;		(* ;; *)
    1.55  by  t;		(* Expr *)
    1.56 @@ -225,8 +225,8 @@
    1.57  Delsplits[split_if];
    1.58  Addsimps[init_vars_def,c_hupd_def,cast_ok_def];
    1.59  Goalw [test_def] 
    1.60 -" \\<lbrakk>new_Addr (heap (snd s0)) = (a, None)\\<rbrakk> \\<Longrightarrow> \
    1.61 -\ tprg\\<turnstile>s0 -test\\<rightarrow> ?s";
    1.62 +" [|new_Addr (heap (snd s0)) = (a, None)|] ==> \
    1.63 +\ tprg\\<turnstile>s0 -test-> ?s";
    1.64  (* ?s = s3 *)
    1.65  by e;		(* ;; *)
    1.66  by  e;		(* Expr *)