src/HOLCF/IOA/meta_theory/RefMappings.ML

--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jun 22 17:12:27 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jun 22 17:13:09 1998 +0200
@@ -15,21 +15,21 @@
 section "transitions and moves";
 
 
-goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
+Goal"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
 
 by (res_inst_tac [("x","(a,t)>>nil")] exI 1);
 by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
 qed"transition_is_ex";
  
 
-goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
+Goal"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
 
 by (res_inst_tac [("x","nil")] exI 1);
 by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
 qed"nothing_is_ex";
 
 
-goal thy"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
+Goal"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
 \        ==> ? ex. move A ex s a s''";
 
 by (res_inst_tac [("x","(a,s')>>(a',s'')>>nil")] exI 1);
@@ -37,7 +37,7 @@
 qed"ei_transitions_are_ex";
 
 
-goal thy
+Goal
 "!!f. (s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
 \     (~a2:ext A) & (~a3:ext A) ==> \
 \     ? ex. move A ex s1 a1 s4";
@@ -52,7 +52,7 @@
 section "weak_ref_map and ref_map";
 
 
-goalw thy [is_weak_ref_map_def,is_ref_map_def]
+Goalw [is_weak_ref_map_def,is_ref_map_def]
   "!!f. [| ext C = ext A; \
 \    is_weak_ref_map f C A |] ==> is_ref_map f C A";
 by (safe_tac set_cs);
@@ -69,7 +69,7 @@
 val lemma = result();
 
 Delsplits [split_if];
-goal thy "!!f.[| is_weak_ref_map f C A |]\
+Goal "!!f.[| is_weak_ref_map f C A |]\
 \                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
 by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
 by (rtac conjI 1);