wneuper/isa: src/Tools/isac/Knowledge/Test.sml@028442673981 (annotated)

neuper@37906	1	val ttt = (term_of o the o (parse thy))
neuper@37991	2	"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e";
neuper@37906	3	val ttt = (term_of o the o (parse thy))
neuper@37991	4	"(Try (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e)";
neuper@37906	5
neuper@37906	6	val ttt = (term_of o the o (parse thy))
neuper@37981	7	"(Rewrite_Set SqRoot_simplify False) e_e ";
neuper@37906	8	val ttt = (term_of o the o (parseold thy))
neuper@37981	9	"%e_. (Rewrite_Set SqRoot_simplify False) e_e";
neuper@37906	10	val ttt = (term_of o the o (parseold thy))
neuper@37981	11	"Repeat (%e_. (Rewrite_Set SqRoot_simplify False)) e_e";
neuper@37906	12
neuper@37906	13	val ttt = (term_of o the o (parse thy))
neuper@37982	14	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37906	15	\[e_]";
neuper@37906	16	val ttt = (term_of o the o (parse thy))
neuper@37982	17	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	18	\((%e_. [e_]) e_e)";
neuper@37906	19	val ttt = (term_of o the o (parse thy))
neuper@37982	20	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	21	\((%e_. (let e_e = e_e in [e_])) e_e)";
neuper@37906	22	val ttt = (term_of o the o (parse thy))
neuper@37982	23	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37906	24	\((%e_. \
neuper@37981	25	\ (let e_e = ((Rewrite_Set SqRoot_simplify False) e_e)\
neuper@37906	26	\ in [e_]))\
neuper@37981	27	\ e_e)";
neuper@37906	28	val ttt = (term_of o the o (parse thy))
neuper@37982	29	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	30	\((%ee_. (let e_e = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_])) e_e)";
neuper@37906	31
neuper@37906	32	val ttt = (term_of o the o (parse thy))
neuper@37982	33	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	34	\(let e_e = \
neuper@37991	35	\ (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\
neuper@37906	36	\ in [e_])";
neuper@37906	37	(----)
neuper@37906	38	val ttt = (term_of o the o (parse thy))
neuper@37906	39
neuper@37906	40	(----)
neuper@37906	41	val ttt = (term_of o the o (parse thy))
neuper@37982	42	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	43	\(let e_e = \
neuper@37906	44	\ (Repeat\
neuper@37991	45	\ ((%ee_. (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\
neuper@37981	46	\ e_e)\
neuper@37981	47	\ e_e)\
neuper@37906	48	\ in [e_])";
neuper@37906	49	val ttt = (term_of o the o (parse thy))
neuper@37982	50	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	51	\(let e_e = \
neuper@37906	52	\ (Repeat\
neuper@37906	53	\ ((%ee_.\
neuper@37991	54	\ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_))\
neuper@37981	55	\ e_e)\
neuper@37981	56	\ e_e)\
neuper@37906	57	\ in [e_])";
neuper@37906	58	val ttt = (term_of o the o (parse thy))
neuper@37982	59	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	60	\(let e_e = \
neuper@37906	61	\ (Repeat\
neuper@37906	62	\ ((%ee_.\
neuper@37991	63	\ (let e_e = ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\
neuper@37981	64	\ in ((Rewrite_Set SqRoot_simplify False) e_e)) )\
neuper@37981	65	\ e_e)\
neuper@37981	66	\ e_e)\
neuper@37906	67	\ in [e_])";
neuper@37906	68	atomty ttt;
neuper@37906	69	atomt ttt;
neuper@37906	70
neuper@37906	71	val ttt = (term_of o the o (parse thy))
neuper@37906	72	"Script Testterm (g_::real) = \
neuper@37906	73	\Repeat\
neuper@37906	74	\ (Rewrite rmult_1 False) g_";
neuper@37906	75	val ttt = (term_of o the o (parse thy))
neuper@37906	76	"Script Testterm (g_::real) = \
neuper@37906	77	\Repeat\
neuper@37906	78	\ (((Rewrite rmult_1 False)) Or ((Rewrite rmult_0 False))) g_";
neuper@37906	79	val ttt = (term_of o the o (parse thy))
neuper@37906	80	"Script Testterm (g_::real) = \
neuper@37906	81	\Repeat\
neuper@37906	82	\ ((Repeat (Rewrite rmult_1 False)) Or (Repeat (Rewrite rmult_0 False))) g_";
neuper@37906	83	val ttt = (term_of o the o (parse thy))
neuper@37906	84	"Script Testterm (g_::real) = \
neuper@37906	85	\Repeat\
neuper@37906	86	\ ((Repeat (Rewrite rmult_1 False)) Or\
neuper@37906	87	\ (Repeat (Rewrite rmult_0 False))) g_";
neuper@37906	88	val ttt = (term_of o the o (parse thy))
neuper@37906	89	"Script Testterm (g_::real) = \
neuper@37906	90	\Repeat\
neuper@37906	91	\ ((Repeat (Rewrite rmult_1 False)) Or\
neuper@37906	92	\ (Repeat (Rewrite rmult_0 False)) Or\
neuper@37906	93	\ (Repeat (Rewrite rmult_0 False))) g_";
neuper@37906	94	val ttt = (term_of o the o (parse thy))
neuper@37906	95	"Script Testterm (g_::real) = \
neuper@37906	96	\Repeat\
neuper@37906	97	\ ((Try Repeat (Rewrite rmult_1 False)) Or\
neuper@37906	98	\ (Try Repeat (Rewrite rmult_0 False)) Or\
neuper@37906	99	\ (Try Repeat (Rewrite rmult_0 False))) g_";
neuper@37906	100
neuper@37906	101
neuper@37906	102
neuper@37906	103
neuper@37906	104
neuper@37906	105
neuper@37906	106
neuper@37906	107
neuper@37906	108
neuper@37906	109
neuper@37906	110
neuper@37906	111
neuper@37906	112
neuper@37906	113	(################### 29.4.02: Rewrite o Rewrite o ...###############)
neuper@37906	114	(################### 29.4.02: Rewrite o Rewrite o ...###############)
neuper@37906	115	(################### 29.4.02: Rewrite o Rewrite o ...###############)
neuper@37906	116
neuper@37906	117
neuper@37906	118
neuper@37906	119	atomt ttt;
neuper@37906	120	val ttt = (term_of o the o (parse thy))
neuper@37982	121	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	122	\(let e_e = \
neuper@37906	123	\ ((Repeat\
neuper@37991	124	\ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
neuper@37981	125	\ (Rewrite_Set SqRoot_simplify False)))) e_e)\
neuper@37906	126	\ in [e_])";
neuper@37906	127	atomty ttt;
neuper@37906	128
neuper@37906	129
neuper@37906	130	val ttt = (term_of o the o (parse thy))
neuper@37991	131	"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy";
neuper@37906	132	atomty ttt;
neuper@37906	133	val ttt = (term_of o the o (parse thy))
neuper@37991	134	"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
neuper@37906	135	\ (Rewrite_Set SqRoot_simplify False)";
neuper@37906	136	atomty ttt;
neuper@37906	137	val ttt = (term_of o the o (parse thy))
neuper@37906	138	"(Repeat\
neuper@37991	139	\ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
neuper@37981	140	\ (Rewrite_Set SqRoot_simplify False))) e_e";
neuper@37906	141	atomty ttt;
neuper@37906	142	val ttt = (term_of o the o (parseold thy))
neuper@37981	143	"(let e_e = Repeat xxx e_e in [e_::bool])";
neuper@37906	144	atomty ttt;
neuper@37906	145	val ttt = (term_of o the o (parseold thy))
neuper@37982	146	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	147	\(let e_e = Repeat (xxx) e_e in [e_::bool])";
neuper@37906	148	atomty ttt;
neuper@37906	149	val ttt = (term_of o the o (parseold thy))
neuper@37982	150	"Script Solve_linear (e_e::bool) (v_v::real)= \
neuper@37981	151	\(let e_e =\
neuper@37906	152	\ Repeat\
neuper@37991	153	\ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
neuper@37906	154	\ (Rewrite_Set SqRoot_simplify False))) e_\
neuper@37906	155	\ in [e_::bool])"
neuper@37906	156	;
neuper@37906	157	atomty ttt;
neuper@37906	158

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 08 Sep 2010 16:47:22 +0200
branch	isac-update-Isa09-2
changeset 37991	028442673981
parent 37982	66f3570ba808
child 37992	351a9e94c38d
permissions	-rw-r--r--